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

Theorem ax10lem16 1665
 Description: Lemma for ax10 1677. Similar to equequ2 1830, without using ax-4 1692, ax-9 1684, ax-10 1678, or ax-12o 1664 but allowing ax-9v 1632. (Contributed by NM, 25-Jul-2015.) (New usage is discouraged.)
Assertion
Ref Expression
ax10lem16

Proof of Theorem ax10lem16
StepHypRef Expression
1 ax12o10lem1 1635 . . 3
2 ax-8 1623 . . . 4
32com12 29 . . 3
41, 3syl5 30 . 2
5 ax12o10lem1 1635 . . 3
6 ax12o10lem1 1635 . . 3
7 ax-8 1623 . . . 4
87com12 29 . . 3
95, 6, 8syl2im 36 . 2
104, 9impbid 185 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178 This theorem is referenced by:  ax10lem21  1670  ax10lem25  1674  ax10lem26  1675  ax9  1683  a12stdy2-x12  27801  a12study4  27806  ax10lem17ALT  27812  ax10lem18ALT  27813 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 This theorem depends on definitions:  df-bi 179
 Copyright terms: Public domain W3C validator