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

Theorem hba1 1721
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 1717 . . 3  |-  ( A. x  -.  A. x ph  ->  -.  A. x ph )
21con2i 114 . 2  |-  ( A. x ph  ->  -.  A. x  -.  A. x ph )
3 ax-6 1704 . 2  |-  ( -. 
A. x  -.  A. x ph  ->  A. x  -.  A. x  -.  A. x ph )
4 ax-6 1704 . . . 4  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
54con1i 123 . . 3  |-  ( -. 
A. x  -.  A. x ph  ->  A. x ph )
65alimi 1547 . 2  |-  ( A. x  -.  A. x  -.  A. x ph  ->  A. x A. x ph )
72, 3, 63syl 20 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6   A.wal 1528
This theorem is referenced by:  spimeh  1724  19.21h  1733  19.12  1736  cbv3hv  1739  nfa1  1758  ax12olem5  1874  ax10lem4  1883  ax9  1891  dvelimfALT  1907  hbra1  2594  hbntal  27591  hbimpg  27592  hbimpgVD  27949  hbalgVD  27950  hbexgVD  27951  a9e2eqVD  27952  e2ebindVD  27957  vk15.4jVD  27959  ax12-2  28371  ax12OLD  28373  hbae-x12  28377  a12study9  28388  a12study5rev  28390  ax10lem18ALT  28392  a12studyALT  28401  a12study3  28403  a12study10  28404  a12study10n  28405  a12study11  28406  a12study11n  28407
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
  Copyright terms: Public domain W3C validator