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

Theorem 3impexpVD 28869
Description: Virtual deduction proof of 3impexp 1375. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
 1:: 2:: 3:1,2,?: e10 28696 4:3,?: e1_ 28629 5:4,?: e1_ 28629 6:5: 7:: 8:7,?: e1_ 28629 9:8,?: e1_ 28629 10:2,9,?: e01 28693 11:10: qed:6,11,?: e00 28781
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
3impexpVD

Proof of Theorem 3impexpVD
StepHypRef Expression
1 idn1 28566 . . . . . 6
2 df-3an 938 . . . . . 6
3 imbi1 314 . . . . . . 7
43biimpcd 216 . . . . . 6
51, 2, 4e10 28696 . . . . 5
6 pm3.3 432 . . . . 5
75, 6e1_ 28629 . . . 4
8 pm3.3 432 . . . 4
97, 8e1_ 28629 . . 3
109in1 28563 . 2
11 idn1 28566 . . . . . 6
12 pm3.31 433 . . . . . 6
1311, 12e1_ 28629 . . . . 5
14 pm3.31 433 . . . . 5
1513, 14e1_ 28629 . . . 4
163biimprd 215 . . . 4
172, 15, 16e01 28693 . . 3
1817in1 28563 . 2
19 bi3 180 . 2
2010, 18, 19e00 28781 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-vd1 28562
 Copyright terms: Public domain W3C validator