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

Theorem exbirVD 28902
Description: Virtual deduction proof of exbir 1374. 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 28773 6:3,5,?: e32 28807 7:6: 8:7: 9:8,?: e1_ 28665 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 28653 . . . . . 6
2 idn1 28602 . . . . . . 7
3 idn2 28651 . . . . . . 7
4 id 20 . . . . . . 7
52, 3, 4e12 28773 . . . . . 6
6 bi2 190 . . . . . . 7
76com12 29 . . . . . 6
81, 5, 7e32 28807 . . . . 5
98in3 28647 . . . 4
109in2 28643 . . 3
11 pm3.3 432 . . 3
1210, 11e1_ 28665 . 2
1312in1 28599 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359 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 28598  df-vd2 28607  df-vd3 28619
 Copyright terms: Public domain W3C validator