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

Theorem hba1 1731
Description:  x is not free in  A. x ph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hba1  |-  ( A. x ph  ->  A. x A. x ph )

Proof of Theorem hba1
StepHypRef Expression
1 sp 1728 . . 3  |-  ( A. x  -.  A. x ph  ->  -.  A. x ph )
21con2i 112 . 2  |-  ( A. x ph  ->  -.  A. x  -.  A. x ph )
3 hbn1 1716 . 2  |-  ( -. 
A. x  -.  A. x ph  ->  A. x  -.  A. x  -.  A. x ph )
4 hbn1 1716 . . . 4  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
54con1i 121 . . 3  |-  ( -. 
A. x  -.  A. x ph  ->  A. x ph )
65alimi 1549 . 2  |-  ( A. x  -.  A. x  -.  A. x ph  ->  A. x A. x ph )
72, 3, 63syl 18 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1530
This theorem is referenced by:  spimeh  1734  19.21h  1743  19.12  1746  cbv3hv  1749  nfa1  1768  ax12olem5  1884  ax10lem4  1894  ax9  1902  dvelimh  1917  hbra1  2605  hbntal  28618  hbimpg  28619  hbimpgVD  28996  hbalgVD  28997  hbexgVD  28998  a9e2eqVD  28999  e2ebindVD  29004  vk15.4jVD  29006  cbv3hvNEW7  29423  19.12vAUX7  29431  ax9NEW7  29445  ax10lem4NEW7  29448  dvelimhvAUX7  29469  dral1NEW7  29470  equs5NEW7  29509  ax7w1AUX7  29615  ax7w2AUX7  29620  ax7w4AUX7  29628  19.12OLD7  29640  dvelimhOLD7  29667  ax12-2  29725  ax12OLD  29727  hbae-x12  29731  a12study9  29742  a12study5rev  29744  ax10lem18ALT  29746  a12studyALT  29755  a12study3  29757  a12study10  29758  a12study10n  29759  a12study11  29760  a12study11n  29761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
  Copyright terms: Public domain W3C validator