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

Theorem ax6e2ndeqVD 37216
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 36847) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2eq 36831 is ax6e2ndeqVD 37216 without virtual deductions and was automatically derived from ax6e2ndeqVD 37216. (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
ax6e2ndeqVD
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem ax6e2ndeqVD
StepHypRef Expression
1 ax6e2nd 36832 . . 3
2 ax6e2eq 36831 . . . 4
31a1d 26 . . . 4
4 exmid 416 . . . 4
5 jao 514 . . . 4
62, 3, 4, 5e000 37064 . . 3
71, 6jaoi 380 . 2
8 idn1 36852 . . . . . . . . . . . . . . . 16
9 idn2 36900 . . . . . . . . . . . . . . . . 17
10 simpl 458 . . . . . . . . . . . . . . . . 17
119, 10e2 36918 . . . . . . . . . . . . . . . 16
12 neeq1 2657 . . . . . . . . . . . . . . . . 17
1312biimprcd 228 . . . . . . . . . . . . . . . 16
148, 11, 13e12 37021 . . . . . . . . . . . . . . 15
15 simpr 462 . . . . . . . . . . . . . . . 16
169, 15e2 36918 . . . . . . . . . . . . . . 15
17 neeq2 2658 . . . . . . . . . . . . . . . 16
1817biimprcd 228 . . . . . . . . . . . . . . 15
1914, 16, 18e22 36958 . . . . . . . . . . . . . 14
20 df-ne 2595 . . . . . . . . . . . . . . . 16
2120bicomi 205 . . . . . . . . . . . . . . 15
22 sp 1914 . . . . . . . . . . . . . . . 16
2322con3i 140 . . . . . . . . . . . . . . 15
2421, 23sylbir 216 . . . . . . . . . . . . . 14
2519, 24e2 36918 . . . . . . . . . . . . 13
2625in2 36892 . . . . . . . . . . . 12
2726gen11 36903 . . . . . . . . . . 11
28 exim 1700 . . . . . . . . . . 11
2927, 28e1a 36914 . . . . . . . . . 10
30 nfnae 2118 . . . . . . . . . . 11
313019.9 1947 . . . . . . . . . 10
32 imbi2 325 . . . . . . . . . . 11
3332biimpcd 227 . . . . . . . . . 10
3429, 31, 33e10 36981 . . . . . . . . 9
3534gen11 36903 . . . . . . . 8
36 exim 1700 . . . . . . . 8
3735, 36e1a 36914 . . . . . . 7
38 excom 1903 . . . . . . 7
39 imbi1 324 . . . . . . . 8
4039biimprcd 228 . . . . . . 7
4137, 38, 40e10 36981 . . . . . 6
42 hbnae 2117 . . . . . . . . 9
4342eximi 1701 . . . . . . . 8
44 nfa1 1956 . . . . . . . . 9
454419.9 1947 . . . . . . . 8
4643, 45sylib 199 . . . . . . 7
47 sp 1914 . . . . . . 7
4846, 47syl 17 . . . . . 6
49 imim1 79 . . . . . 6
5041, 48, 49e10 36981 . . . . 5
51 orc 386 . . . . . 6
5251imim2i 16 . . . . 5
5350, 52e1a 36914 . . . 4
5453in1 36849 . . 3
55 idn1 36852 . . . . . 6
56 ax-1 6 . . . . . 6
5755, 56e1a 36914 . . . . 5
58 olc 385 . . . . . 6
5958imim2i 16 . . . . 5
6057, 59e1a 36914 . . . 4
6160in1 36849 . . 3
62 exmidne 2604 . . 3
63 jao 514 . . . 4
6463com12 32 . . 3
6554, 61, 62, 64e000 37064 . 2
667, 65impbii 190 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370  wal 1435   wceq 1437  wex 1657   wne 2593 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-ne 2595  df-v 3018  df-vd1 36848  df-vd2 36856 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator