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

Theorem orbi1rVD 37238
Description: Virtual deduction proof of orbi1r 36860. 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:2,?: e2 37004 4:1,3,?: e12 37105 5:4,?: e2 37004 6:5: 7:: 8:7,?: e2 37004 9:1,8,?: e12 37105 10:9,?: e2 37004 11:10: 12:6,11,?: e11 37061 qed:12:
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
orbi1rVD

Proof of Theorem orbi1rVD
StepHypRef Expression
1 idn1 36938 . . . . . 6
2 idn2 36986 . . . . . . 7
3 pm1.4 388 . . . . . . 7
42, 3e2 37004 . . . . . 6
5 orbi1 711 . . . . . . 7
65biimpd 211 . . . . . 6
71, 4, 6e12 37105 . . . . 5
8 pm1.4 388 . . . . 5
97, 8e2 37004 . . . 4
109in2 36978 . . 3
11 idn2 36986 . . . . . . 7
12 pm1.4 388 . . . . . . 7
1311, 12e2 37004 . . . . . 6
145biimprd 227 . . . . . 6
151, 13, 14e12 37105 . . . . 5
16 pm1.4 388 . . . . 5
1715, 16e2 37004 . . . 4
1817in2 36978 . . 3
19 impbi 190 . . 3
2010, 18, 19e11 37061 . 2
2120in1 36935 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wo 370 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-vd1 36934  df-vd2 36942 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator