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

Theorem mo2OLD 2336
 Description: Obsolete proof of mo2 2287 as of 28-May-2019. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
mo2OLD.1
Assertion
Ref Expression
mo2OLD
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem mo2OLD
StepHypRef Expression
1 df-mo 2280 . 2
2 alnex 1598 . . . . 5
3 pm2.21 108 . . . . . . 7
43alimi 1614 . . . . . 6
5 19.8a 1806 . . . . . 6
64, 5syl 16 . . . . 5
72, 6sylbir 213 . . . 4
8 mo2OLD.1 . . . . 5
98eumo0OLD 2313 . . . 4
107, 9ja 161 . . 3
118eu3OLD 2330 . . . 4
1211simplbi2com 627 . . 3
1310, 12impbii 188 . 2
141, 13bitri 249 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184  wal 1377  wex 1596  wnf 1599  weu 2275  wmo 2276 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator