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

Theorem orbi1rVD 28960
Description: Virtual deduction proof of orbi1r 28592. 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 28732 4:1,3,?: e12 28836 5:4,?: e2 28732 6:5: 7:: 8:7,?: e2 28732 9:1,8,?: e12 28836 10:9,?: e2 28732 11:10: 12:6,11,?: e11 28789 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 28665 . . . . . 6
2 idn2 28714 . . . . . . 7
3 pm1.4 376 . . . . . . 7
42, 3e2 28732 . . . . . 6
5 orbi1 687 . . . . . . 7
65biimpd 199 . . . . . 6
71, 4, 6e12 28836 . . . . 5
8 pm1.4 376 . . . . 5
97, 8e2 28732 . . . 4
109in2 28706 . . 3
11 idn2 28714 . . . . . . 7
12 pm1.4 376 . . . . . . 7
1311, 12e2 28732 . . . . . 6
145biimprd 215 . . . . . 6
151, 13, 14e12 28836 . . . . 5
16 pm1.4 376 . . . . 5
1715, 16e2 28732 . . . 4
1817in2 28706 . . 3
19 bi3 180 . . 3
2010, 18, 19e11 28789 . 2
2120in1 28662 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wo 358 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-or 360  df-an 361  df-vd1 28661  df-vd2 28670
 Copyright terms: Public domain W3C validator