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

Theorem onfrALTVD 30473
Description: Virtual deduction proof of onfrALT 30103. 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 30103 is onfrALTVD 30473 without virtual deductions and was automatically derived from onfrALTVD 30473.
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 30133 . . . . . 6
2 simpr 449 . . . . . 6
31, 2e1_ 30196 . . . . 5
4 exmid 406 . . . . . . . . . 10
5 onfrALTlem1VD 30472 . . . . . . . . . . 11
65in2an 30177 . . . . . . . . . 10
7 onfrALTlem2VD 30471 . . . . . . . . . . 11
87in2an 30177 . . . . . . . . . 10
9 pm2.61 166 . . . . . . . . . . 11
109a1i 11 . . . . . . . . . 10
114, 6, 8, 10e022 30210 . . . . . . . . 9
1211in2 30174 . . . . . . . 8
1312gen11 30185 . . . . . . 7
14 19.23v 1918 . . . . . . . 8
1514biimpi 188 . . . . . . 7
1613, 15e1_ 30196 . . . . . 6
17 n0 3682 . . . . . 6
18 imbi1 315 . . . . . . 7
1918biimprcd 218 . . . . . 6
2016, 17, 19e10 30263 . . . . 5
21 pm2.27 38 . . . . 5
223, 20, 21e11 30257 . . . 4
2322in1 30130 . . 3
2423ax-gen 1570 . 2
25 dfepfr 4726 . . 3
2625biimpri 199 . 2
2724, 26e0_ 30352 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  \/wo 359  /\wa 360  A.wal 1564  E.wex 1565  =wceq 1670  e.wcel 1732  =/=wne 2652  E.wrex 2760  i^icin 3364  C_wss 3365   c0 3673   cep 4651  Frwfr 4697   con0 4740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pr 4554
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1338  df-fal 1339  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-nul 3674  df-if 3826  df-sn 3915  df-pr 3916  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-tr 4412  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-vd1 30129  df-vd2 30138  df-vd3 30150
  Copyright terms: Public domain W3C validator