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

Theorem onfrALTVD 30196
Description: Virtual deduction proof of onfrALT 29826. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALT 29826 is onfrALTVD 30196 without virtual deductions and was automatically derived from onfrALTVD 30196.
1:: |-(.( C_ /\ =/= ),.( e. /\-.( i^i )= )->.E. e. ( i^i )= ).
2:: |-(.( C_ /\ =/= ),.( e. /\( i^i )= )->.E. e. ( i^i )= ).
3:1: |-(.( C_ /\ =/= ),. e. ->. (-.( i^i )= ->E. e. ( i^i )= )).
4:2: |-(.( C_ /\ =/= ),. e. ->. (( i^i )= ->E. e. ( i^i )= )).
5:: |-(( i^i )= \/-.( i^i )= )
6:5,4,3: |-(.( C_ /\ =/= ),. e. ->. E. e. ( i^i )= ).
7:6: |-(.( C_ /\ =/= )->.( e. ->E. e. ( i^i )= )).
8:7: |-(.( C_ /\ =/= )->.A. ( e. ->E. e. ( i^i )= )).
9:8: |-(.( C_ /\ =/= )->.(E. e. ->E. e. ( i^i )= )).
10:: |-( =/= <->E. e. )
11:9,10: |-(.( C_ /\ =/= )->.( =/= ->E. e. ( i^i )= )).
12:: |-(.( C_ /\ =/= )->.( C_ /\ =/= )).
13:12: |-(.( C_ /\ =/= )->. =/= ).
14:13,11: |-(.( C_ /\ =/= )->.E. e. ( i^i )= ).
15:14: |-(( C_ /\ =/= )->E. e. ( i^i )= )
16:15: |-A. (( C_ /\ =/= )->E. e. ( i^i )= )
qed:16: |- Fr
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTVD

Proof of Theorem onfrALTVD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 29856 . . . . . 6
2 simpr 449 . . . . . 6
31, 2e1_ 29919 . . . . 5
4 exmid 406 . . . . . . . . . 10
5 onfrALTlem1VD 30195 . . . . . . . . . . 11
65in2an 29900 . . . . . . . . . 10
7 onfrALTlem2VD 30194 . . . . . . . . . . 11
87in2an 29900 . . . . . . . . . 10
9 pm2.61 166 . . . . . . . . . . 11
109a1i 11 . . . . . . . . . 10
114, 6, 8, 10e022 29933 . . . . . . . . 9
1211in2 29897 . . . . . . . 8
1312gen11 29908 . . . . . . 7
14 19.23v 1910 . . . . . . . 8
1514biimpi 188 . . . . . . 7
1613, 15e1_ 29919 . . . . . 6
17 n0 3669 . . . . . 6
18 imbi1 315 . . . . . . 7
1918biimprcd 218 . . . . . 6
2016, 17, 19e10 29986 . . . . 5
21 pm2.27 38 . . . . 5
223, 20, 21e11 29980 . . . 4
2322in1 29853 . . 3
2423ax-gen 1562 . 2
25 dfepfr 4708 . . 3
2625biimpri 199 . 2
2724, 26e0_ 30075 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  \/wo 359  /\wa 360  A.wal 1556  E.wex 1557  =wceq 1662  e.wcel 1724  =/=wne 2644  E.wrex 2752  i^icin 3352  C_wss 3353   c0 3660   cep 4633  Frwfr 4679   con0 4722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pr 4538
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1337  df-fal 1338  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-nul 3661  df-if 3813  df-sn 3900  df-pr 3901  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-tr 4396  df-eprel 4635  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-vd1 29852  df-vd2 29861  df-vd3 29873
  Copyright terms: Public domain W3C validator