Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax9lem9 Unicode version

Theorem ax9lem9 29148
 Description: Lemma for ax9 1889. Similar to hbimd 1721, without using sp 1716, ax9 1889, or ax10 1884. (Contributed by NM, 7-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ax9lem9.a
ax9lem9.c
ax9lem9.1
ax9lem9.2
ax9lem9.3
Assertion
Ref Expression
ax9lem9
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem ax9lem9
StepHypRef Expression
1 ax9lem9.1 . . . . 5
2 ax9lem9.2 . . . . 5
31, 2alrimih 1552 . . . 4
4 ax9lem9.a . . . . . . 7
5 ax9lem9.c . . . . . . 7
64, 5ax9lem3 29142 . . . . . 6
7 hbn1 1704 . . . . . 6
86, 7nsyl4 134 . . . . 5
98con1i 121 . . . 4
10 con3 126 . . . . 5
1110al2imi 1548 . . . 4
123, 9, 11syl2im 34 . . 3
13 pm2.21 100 . . . 4
1413alimi 1546 . . 3
1512, 14syl6 29 . 2
16 ax9lem9.3 . . 3
17 ax-1 5 . . . 4
1817alimi 1546 . . 3
1916, 18syl6 29 . 2