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  ax12o10lem2X  28283  ax12o10lem3X  28284  ax12olem21X  28322  ax12olem26X  28331  ax12olem27X  28332  ax10lem16X  28335  ax10X  28347  a16gALTX  28348  hbae-x12  28359  a12stdy2-x12  28362  equvinv  28364  equvelv  28366  ax10lem18ALT  28374  a12study10n  28387 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