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

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

Proof of Theorem a9e2ndVD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 2961 . . . . . . 7
2 a9e 1953 . . . . . . 7
31, 2pm3.2i 443 . . . . . 6
4 19.42v 1929 . . . . . . 7
54biimpri 199 . . . . . 6
63, 5e0_ 28886 . . . . 5
7 isset 2962 . . . . . . 7
87anbi1i 678 . . . . . 6
98exbii 1593 . . . . 5
106, 9mpbi 201 . . . 4
11 idn1 28667 . . . . . 6
12 hbnae 2044 . . . . . . 7
13 hbn1 1746 . . . . . . . . . . . 12
14 ax-17 1627 . . . . . . . . . . . . . . . 16
15 ax-17 1627 . . . . . . . . . . . . . . . 16
16 idn1 28667 . . . . . . . . . . . . . . . . . 18
17 equequ1 1697 . . . . . . . . . . . . . . . . . 18
1816, 17e1_ 28730 . . . . . . . . . . . . . . . . 17
1918in1 28664 . . . . . . . . . . . . . . . 16
2014, 15, 19dvelimh 2072 . . . . . . . . . . . . . . 15
2111, 20e1_ 28730 . . . . . . . . . . . . . 14
2221in1 28664 . . . . . . . . . . . . 13
2322alimi 1569 . . . . . . . . . . . 12
2413, 23syl 16 . . . . . . . . . . 11
2511, 24e1_ 28730 . . . . . . . . . 10
26 19.41rg 28639 . . . . . . . . . 10
2725, 26e1_ 28730 . . . . . . . . 9
2827in1 28664 . . . . . . . 8
2928alimi 1569 . . . . . . 7
3012, 29syl 16 . . . . . 6
3111, 30e1_ 28730 . . . . 5
32 exim 1585 . . . . 5
3331, 32e1_ 28730 . . . 4
34 pm2.27 38 . . . 4
3510, 33, 34e01 28794 . . 3
36 excomim 1758 . . 3
3735, 36e1_ 28730 . 2
3837in1 28664 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360  wal 1550  wex 1551   wceq 1653   wcel 1726  cvv 2958 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-v 2960  df-vd1 28663
 Copyright terms: Public domain W3C validator