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

Theorem ax12o10lem1 1635
 Description: Lemma for ax12o 1663 and ax10 1677. Same as equcomi 1822, without using ax-4 1692, ax-9 1684, ax-10 1678, or ax-12o 1664 but allowing ax-9v 1632. Note that in these lemmas we use ax-9v 1632 instead of ax-9 1684 since the proof of ax9 1683 from ax-9v 1632 makes use of ax-12o 1664. The first use of ax-12o 1664 occurs in ax10lem24 1673. (Contributed by NM, 25-Jul-2015.) (New usage is discouraged.)
Assertion
Ref Expression
ax12o10lem1

Proof of Theorem ax12o10lem1
StepHypRef Expression
1 ax-9v 1632 . . . 4
2 ax-8 1623 . . . . . . 7
32pm2.43i 45 . . . . . 6
43con3i 129 . . . . 5
54alimi 1546 . . . 4
61, 5mto 169 . . 3
7 ax-17 1628 . . 3
86, 7mt3 173 . 2
9 ax-8 1623 . 2
108, 9mpi 18 1
 Colors of variables: wff set class Syntax hints:   wn 5   wi 6  wal 1532 This theorem is referenced by:  ax12o10lem2  1636  ax12o10lem3  1637  ax12olem21  1655  ax12olem26  1660  ax12olem27  1661  ax10lem16  1665  ax10  1677  a16gALT  1679  hbae-x12  27798  a12stdy2-x12  27801  equvinv  27803  equvelv  27805  ax10lem18ALT  27813  a12study10n  27826 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9v 1632
 Copyright terms: Public domain W3C validator