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

Theorem hbn1 1704
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 1703 1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1527
This theorem is referenced by:  hbe1  1705  modal-5  1707  ax5o  1717  hba1  1719  hbn  1720  hbimd  1721  dvelimhw  1735  ax12olem6  1873  dvelimv  1879  a16g  1885  ax15  1961  dvelimALT  2072  ax11indn  2134  vk15.4j  28291  a9e2nd  28324  a9e2ndVD  28684  a9e2ndALT  28707  ax12OLD  29105  a12study9  29120  ax10lem17ALT  29123  dvelimfALT2OLD  29125  a12studyALT  29133  a12study2  29134  a12study3  29135  ax9lem4  29143  ax9lem7  29146  ax9lem8  29147  ax9lem9  29148  ax9lem17  29156
This theorem was proved from axioms:  ax-6 1703
  Copyright terms: Public domain W3C validator