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

Theorem hba1 1719
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 1716 . . 3  |-  ( A. x  -.  A. x ph  ->  -.  A. x ph )
21con2i 112 . 2  |-  ( A. x ph  ->  -.  A. x  -.  A. x ph )
3 hbn1 1704 . 2  |-  ( -. 
A. x  -.  A. x ph  ->  A. x  -.  A. x  -.  A. x ph )
4 hbn1 1704 . . . 4  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
54con1i 121 . . 3  |-  ( -. 
A. x  -.  A. x ph  ->  A. x ph )
65alimi 1546 . 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 1527
This theorem is referenced by:  spimeh  1722  19.21h  1731  19.12  1734  cbv3hv  1737  nfa1  1756  ax12olem5  1872  ax10lem4  1881  ax9  1889  dvelimh  1904  hbra1  2592  hbntal  28319  hbimpg  28320  hbimpgVD  28680  hbalgVD  28681  hbexgVD  28682  a9e2eqVD  28683  e2ebindVD  28688  vk15.4jVD  28690  ax12-2  29103  ax12OLD  29105  hbae-x12  29109  a12study9  29120  a12study5rev  29122  ax10lem18ALT  29124  a12studyALT  29133  a12study3  29135  a12study10  29136  a12study10n  29137  a12study11  29138  a12study11n  29139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
  Copyright terms: Public domain W3C validator