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

Theorem moOLD 2320
 Description: Obsolete proof of mo 2315 as of 7-Oct-2018. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
moOLD.1
Assertion
Ref Expression
moOLD
Distinct variable group:   ,
Allowed substitution hints:   (,)

Proof of Theorem moOLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 moOLD.1 . . . . . 6
2 nfv 1678 . . . . . 6
31, 2nfim 1862 . . . . 5
43nfal 1889 . . . 4
5 nfv 1678 . . . 4
6 equequ2 1743 . . . . . 6
76imbi2d 316 . . . . 5
87albidv 1684 . . . 4
94, 5, 8cbvex 1988 . . 3
10 nfs1v 2157 . . . . . . . . 9
11 nfv 1678 . . . . . . . . 9
1210, 11nfim 1862 . . . . . . . 8
13 sbequ2 1708 . . . . . . . . 9
14 ax-7 1734 . . . . . . . . 9
1513, 14imim12d 74 . . . . . . . 8
163, 12, 15cbv3 1977 . . . . . . 7
1716ancli 551 . . . . . 6
183, 12aaan 1919 . . . . . 6
1917, 18sylibr 212 . . . . 5
20 prth 571 . . . . . . 7
21 equtr2 1746 . . . . . . 7
2220, 21syl6 33 . . . . . 6
23222alimi 1610 . . . . 5
2419, 23syl 16 . . . 4
2524exlimiv 1693 . . 3
269, 25sylbir 213 . 2
27 nfa2 1895 . . . 4
28 sp 1803 . . . . . . . 8
2928expd 436 . . . . . . 7
3029com3r 79 . . . . . 6
3110, 30alimd 1819 . . . . 5
3231com12 31 . . . 4
3327, 32eximd 1825 . . 3
34 alnex 1593 . . . 4
3510nfn 1844 . . . . . 6
361nfn 1844 . . . . . 6
37 sbequ1 1953 . . . . . . . 8
3837equcoms 1739 . . . . . . 7
3938con3d 133 . . . . . 6
4035, 36, 39cbv3 1977 . . . . 5
41 pm2.21 108 . . . . . 6
4241alimi 1609 . . . . 5
43 19.8a 1801 . . . . 5
4440, 42, 433syl 20 . . . 4
4534, 44sylbir 213 . . 3
4633, 45pm2.61d1 159 . 2
4726, 46impbii 188 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369  wal 1372  wex 1591  wnf 1594  wsb 1706 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1707 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator