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

Theorem onfrALTVD 29400
Description: Virtual deduction proof of onfrALT 29030. 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 29030 is onfrALTVD 29400 without virtual deductions and was automatically derived from onfrALTVD 29400.
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 29060 . . . . . 6
2 simpr 449 . . . . . 6
31, 2e1_ 29123 . . . . 5
4 exmid 406 . . . . . . . . . 10
5 onfrALTlem1VD 29399 . . . . . . . . . . 11
65in2an 29104 . . . . . . . . . 10
7 onfrALTlem2VD 29398 . . . . . . . . . . 11
87in2an 29104 . . . . . . . . . 10
9 pm2.61 166 . . . . . . . . . . 11
109a1i 11 . . . . . . . . . 10
114, 6, 8, 10e022 29137 . . . . . . . . 9
1211in2 29101 . . . . . . . 8
1312gen11 29112 . . . . . . 7
14 19.23v 1919 . . . . . . . 8
1514biimpi 188 . . . . . . 7
1613, 15e1_ 29123 . . . . . 6
17 n0 3629 . . . . . 6
18 imbi1 315 . . . . . . 7
1918biimprcd 218 . . . . . 6
2016, 17, 19e10 29190 . . . . 5
21 pm2.27 38 . . . . 5
223, 20, 21e11 29184 . . . 4
2322in1 29057 . . 3
2423ax-gen 1556 . 2
25 dfepfr 4612 . . 3
2625biimpri 199 . 2
2724, 26e0_ 29279 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  \/wo 359  /\wa 360  A.wal 1550  E.wex 1551  =wceq 1654  e.wcel 1728  =/=wne 2610  E.wrex 2717  i^icin 3312  C_wss 3313   c0 3620   cep 4537  Frwfr 4583   con0 4626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-sep 4368  ax-nul 4376  ax-pr 4446
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-ral 2721  df-rex 2722  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3621  df-if 3770  df-sn 3851  df-pr 3852  df-op 3854  df-uni 4048  df-br 4248  df-opab 4306  df-tr 4341  df-eprel 4539  df-po 4548  df-so 4549  df-fr 4586  df-we 4588  df-ord 4629  df-on 4630  df-vd1 29056  df-vd2 29065  df-vd3 29077
  Copyright terms: Public domain W3C validator