MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hbn1 Unicode version

Theorem hbn1 1735
Description:  x is not free in  -.  A. x ph. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
Assertion
Ref Expression
hbn1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )

Proof of Theorem hbn1
StepHypRef Expression
1 ax-6 1734 1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1545
This theorem is referenced by:  hbe1  1736  modal-5  1738  ax5o  1755  hbnOLD  1783  hba1OLD  1793  hbimdOLD  1823  dvelimhw  1859  ax12olem6  1945  dvelimv  1952  a16g  1958  ax15  2034  dvelimALT  2146  ax11indn  2208  vk15.4j  28026  a9e2nd  28059  a9e2ndVD  28436  a9e2ndALT  28459  dvelimhwNEW7  28868  ax12olem6NEW7  28872  dvelimvNEW7  28875  dvelimhvAUX7  28905  equs5NEW7  28945  ax15NEW7  28947  a16gNEW7  28957  dvelimALTNEW7  29044  ax12OLD  29164  a12study9  29179  ax10lem17ALT  29182  dvelimfALT2OLD  29184  a12studyALT  29192  a12study2  29193  a12study3  29194  ax9lem4  29202  ax9lem7  29205  ax9lem8  29206  ax9lem9  29207  ax9lem17  29215
This theorem was proved from axioms:  ax-6 1734
  Copyright terms: Public domain W3C validator