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

Theorem 3impexpVD 37226
Description: Virtual deduction proof of 3impexp 1227. 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 37045 4:3,?: e1a 36978 5:4,?: e1a 36978 6:5: 7:: 8:7,?: e1a 36978 9:8,?: e1a 36978 10:2,9,?: e01 37042 11:10: qed:6,11,?: e00 37129
(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 36916 . . . . . 6
2 df-3an 984 . . . . . 6
3 imbi1 324 . . . . . . 7
43biimpcd 227 . . . . . 6
51, 2, 4e10 37045 . . . . 5
6 pm3.3 445 . . . . 5
75, 6e1a 36978 . . . 4
8 pm3.3 445 . . . 4
97, 8e1a 36978 . . 3
109in1 36913 . 2
11 idn1 36916 . . . . . 6
12 pm3.31 446 . . . . . 6
1311, 12e1a 36978 . . . . 5
14 pm3.31 446 . . . . 5
1513, 14e1a 36978 . . . 4
163biimprd 226 . . . 4
172, 15, 16e01 37042 . . 3
1817in1 36913 . 2
19 impbi 189 . 2
2010, 18, 19e00 37129 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-vd1 36912 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator