Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  a9e2ndeqVD Unicode version

Theorem a9e2ndeqVD 29001
Description: The following User's Proof is a Virtual Deduction proof (see: wvd1 28636) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. a9e2eq 28622 is a9e2ndeqVD 29001 without virtual deductions and was automatically derived from a9e2ndeqVD 29001. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 1:: 2:: 3:2: 4:1,3: 5:2: 6:4,5: 7:: 8:7: 9:: 10:8,9: 11:6,10: 12:11: 13:12: 14:13: 15:: 19:15: 20:14,19: 21:20: 22:21: 23:: 24:22,23: 25:: 26:25: 260:: 27:260: 270:26,27: 28:: 29:270,28: 30:24,29: 31:30: 32:31: 33:: 34:33: 35:34: 36:35: 37:: 38:32,36,37: 39:: 40:: 41:40: 42:: 43:39,41,42: 44:40,43: qed:38,44:
Assertion
Ref Expression
a9e2ndeqVD
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem a9e2ndeqVD
StepHypRef Expression
1 a9e2nd 28623 . . 3
2 a9e2eq 28622 . . . 4
31a1d 22 . . . 4
4 exmid 404 . . . 4
5 jao 498 . . . 4
62, 3, 4, 5e000 28856 . . 3
71, 6jaoi 368 . 2
8 idn1 28641 . . . . . . . . . . . . . . . 16
9 idn2 28690 . . . . . . . . . . . . . . . . 17
10 simpl 443 . . . . . . . . . . . . . . . . 17
119, 10e2 28708 . . . . . . . . . . . . . . . 16
12 neeq1 2467 . . . . . . . . . . . . . . . . 17
1312biimprcd 216 . . . . . . . . . . . . . . . 16
148, 11, 13e12 28813 . . . . . . . . . . . . . . 15
15 simpr 447 . . . . . . . . . . . . . . . 16
169, 15e2 28708 . . . . . . . . . . . . . . 15
17 neeq2 2468 . . . . . . . . . . . . . . . 16
1817biimprcd 216 . . . . . . . . . . . . . . 15
1914, 16, 18e22 28748 . . . . . . . . . . . . . 14
20 df-ne 2461 . . . . . . . . . . . . . . . 16
2120bicomi 193 . . . . . . . . . . . . . . 15
22 sp 1728 . . . . . . . . . . . . . . . 16
2322con3i 127 . . . . . . . . . . . . . . 15
2421, 23sylbir 204 . . . . . . . . . . . . . 14
2519, 24e2 28708 . . . . . . . . . . . . 13
2625in2 28682 . . . . . . . . . . . 12
2726gen11 28693 . . . . . . . . . . 11
28 exim 1565 . . . . . . . . . . 11
2927, 28e1_ 28704 . . . . . . . . . 10
30 nfnae 1909 . . . . . . . . . . 11
313019.9 1795 . . . . . . . . . 10
32 imbi2 314 . . . . . . . . . . 11
3332biimpcd 215 . . . . . . . . . 10
3429, 31, 33e10 28772 . . . . . . . . 9
3534gen11 28693 . . . . . . . 8
36 exim 1565 . . . . . . . 8
3735, 36e1_ 28704 . . . . . . 7
38 excom 1798 . . . . . . 7
39 imbi1 313 . . . . . . . 8
4039biimprcd 216 . . . . . . 7
4137, 38, 40e10 28772 . . . . . 6
42 hbnae 1908 . . . . . . . . 9
4342eximi 1566 . . . . . . . 8
44 nfa1 1768 . . . . . . . . 9
454419.9 1795 . . . . . . . 8
4643, 45sylib 188 . . . . . . 7
47 sp 1728 . . . . . . 7
4846, 47syl 15 . . . . . 6
49 imim1 70 . . . . . 6
5041, 48, 49e10 28772 . . . . 5
51 orc 374 . . . . . 6
5251imim2i 13 . . . . 5
5350, 52e1_ 28704 . . . 4
5453in1 28638 . . 3
55 idn1 28641 . . . . . 6
56 ax-1 5 . . . . . 6
5755, 56e1_ 28704 . . . . 5
58 olc 373 . . . . . 6
5958imim2i 13 . . . . 5
6057, 59e1_ 28704 . . . 4
6160in1 28638 . . 3
62 exmidne 2465 . . 3
63 jao 498 . . . 4
6463com12 27 . . 3
6554, 61, 62, 64e000 28856 . 2
667, 65impbii 180 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358  wal 1530  wex 1531   wceq 1632   wne 2459 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ne 2461  df-v 2803  df-vd1 28637  df-vd2 28646
 Copyright terms: Public domain W3C validator