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

Theorem 3ornot23VD 37243
Description: Virtual deduction proof of 3ornot23 36865. 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,?: e1a 37006 4:1,?: e1a 37006 5:3,4,?: e11 37067 6:2,?: e2 37010 7:5,6,?: e12 37111 8:7: qed:8:
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
3ornot23VD

Proof of Theorem 3ornot23VD
StepHypRef Expression
1 idn1 36944 . . . . . 6
2 simpl 459 . . . . . 6
31, 2e1a 37006 . . . . 5
4 simpr 463 . . . . . 6
51, 4e1a 37006 . . . . 5
6 ioran 493 . . . . . 6
76simplbi2 631 . . . . 5
83, 5, 7e11 37067 . . . 4
9 idn2 36992 . . . . 5
10 3orass 988 . . . . . 6
1110biimpi 198 . . . . 5
129, 11e2 37010 . . . 4
13 orel2 385 . . . 4
148, 12, 13e12 37111 . . 3
1514in2 36984 . 2
1615in1 36941 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 370   wa 371   w3o 984 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 189  df-or 372  df-an 373  df-3or 986  df-vd1 36940  df-vd2 36948 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator