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

Theorem hbn1 1746
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 1745 1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1550
This theorem is referenced by:  hbe1  1747  modal-5  1749  ax5o  1766  hbnOLD  1803  hba1OLD  1806  hbimdOLD  1836  dvelimhwOLD  1878  ax12olem6OLD  2017  dvelimvOLD  2029  a16gOLD  2050  ax15  2109  dvelimALT  2212  ax11indn  2274  vk15.4j  28686  a9e2nd  28719  a9e2ndVD  29094  a9e2ndALT  29116  dvelimhwNEW7  29529  ax12olem6NEW7  29533  dvelimvNEW7  29536  dvelimhvAUX7  29566  equs5NEW7  29608  ax15NEW7  29610  a16gNEW7  29620  dvelimALTNEW7  29710
This theorem was proved from axioms:  ax-6 1745
  Copyright terms: Public domain W3C validator