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

Theorem ax16iNEW7 29255
 Description: Inference with ax16 2094 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ax16i.1NEW
ax16i.2NEW
Assertion
Ref Expression
ax16iNEW7
Distinct variable groups:   ,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem ax16iNEW7
StepHypRef Expression
1 nfv 1626 . . 3
2 nfv 1626 . . 3
3 ax-8 1683 . . 3
41, 2, 3cbv3wAUX7 29221 . 2
5 ax-8 1683 . . . . 5
65spimvNEW7 29225 . . . 4
7 equcomi 1687 . . . . . 6
8 equcomi 1687 . . . . . . 7
9 ax-8 1683 . . . . . . 7
108, 9syl 16 . . . . . 6
117, 10syl5com 28 . . . . 5
1211alimdv 1628 . . . 4
136, 12mpcom 34 . . 3
14 equcomi 1687 . . . 4
1514alimi 1565 . . 3
1613, 15syl 16 . 2
17 ax16i.1NEW . . . . 5
1817biimpcd 216 . . . 4
1918alimdv 1628 . . 3
20 ax16i.2NEW . . . . 5
2120nfi 1557 . . . 4
22 nfv 1626 . . . 4
2317biimprd 215 . . . . 5
2414, 23syl 16 . . . 4
2521, 22, 24cbv3wAUX7 29221 . . 3
2619, 25syl6com 33 . 2
274, 16, 263syl 19 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wal 1546 This theorem is referenced by:  ax16ALTNEW7  29336 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757  ax-12 1946  ax-7v 29148 This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
 Copyright terms: Public domain W3C validator