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

Theorem exbirVD 33386
Description: Virtual deduction proof of exbir 32952. 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:: 5:1,2,?: e12 33254 6:3,5,?: e32 33288 7:6: 8:7: 9:8,?: e1a 33146 qed:9:
(Contributed by Alan Sare, 13-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
exbirVD

Proof of Theorem exbirVD
StepHypRef Expression
1 idn3 33134 . . . . . 6
2 idn1 33084 . . . . . . 7
3 idn2 33132 . . . . . . 7
4 id 22 . . . . . . 7
52, 3, 4e12 33254 . . . . . 6
6 bi2 198 . . . . . . 7
76com12 31 . . . . . 6
81, 5, 7e32 33288 . . . . 5
98in3 33128 . . . 4
109in2 33124 . . 3
11 pm3.3 444 . . 3
1210, 11e1a 33146 . 2
1312in1 33081 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369 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 185  df-an 371  df-3an 976  df-vd1 33080  df-vd2 33088  df-vd3 33100 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator