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

Theorem ax6e2ndVD 37368
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 37007) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd 36995 is ax6e2ndVD 37368 without virtual deductions and was automatically derived from ax6e2ndVD 37368. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 1:: 2:: 3:1,2: 4:3: 5:: 6:5: 7:6: 8:4,7: 9:: 10:: 11:: 12:11: 120:11: 13:9,10,120: 14:: 15:14,13: 16:15: 17:16: 18:: 19:17,18: 20:14,19: 21:20: 22:21: 23:22: 24:: 25:23,24: 26:14,25: 27:26: 28:8,27: 29:28: qed:29:
Assertion
Ref Expression
ax6e2ndVD
Distinct variable groups:   ,   ,   ,

Proof of Theorem ax6e2ndVD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 3034 . . . . . . 7
2 ax6e 2107 . . . . . . 7
31, 2pm3.2i 462 . . . . . 6
4 19.42v 1842 . . . . . . 7
54biimpri 211 . . . . . 6
63, 5e0a 37222 . . . . 5
7 isset 3035 . . . . . . 7
87anbi1i 709 . . . . . 6
98exbii 1726 . . . . 5
106, 9mpbi 213 . . . 4
11 idn1 37012 . . . . . 6
12 hbnae 2166 . . . . . . 7
13 hbn1 1933 . . . . . . . . . . . 12
14 ax-5 1766 . . . . . . . . . . . . . . . 16
15 ax-5 1766 . . . . . . . . . . . . . . . 16
16 idn1 37012 . . . . . . . . . . . . . . . . . 18
17 equequ1 1875 . . . . . . . . . . . . . . . . . 18
1816, 17e1a 37074 . . . . . . . . . . . . . . . . 17
1918in1 37009 . . . . . . . . . . . . . . . 16
2014, 15, 19dvelimh 2185 . . . . . . . . . . . . . . 15
2111, 20e1a 37074 . . . . . . . . . . . . . 14
2221in1 37009 . . . . . . . . . . . . 13
2322alimi 1692 . . . . . . . . . . . 12
2413, 23syl 17 . . . . . . . . . . 11
2511, 24e1a 37074 . . . . . . . . . 10
26 19.41rg 36987 . . . . . . . . . 10
2725, 26e1a 37074 . . . . . . . . 9
2827in1 37009 . . . . . . . 8
2928alimi 1692 . . . . . . 7
3012, 29syl 17 . . . . . 6
3111, 30e1a 37074 . . . . 5
32 exim 1714 . . . . 5
3331, 32e1a 37074 . . . 4
34 pm2.27 39 . . . 4
3510, 33, 34e01 37138 . . 3
36 excomim 1946 . . 3
3735, 36e1a 37074 . 2
3837in1 37009 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wa 376  wal 1450   wceq 1452  wex 1671   wcel 1904  cvv 3031 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-v 3033  df-vd1 37008 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator