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

Theorem sbc3orgVD 29037
Description: Virtual deduction proof of sbc3org 28690. 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:1,?: e1_ 28802 3:: 32:3: 33:1,32,?: e10 28869 4:1,33,?: e11 28863 5:2,4,?: e11 28863 6:1,?: e1_ 28802 7:6,?: e1_ 28802 8:5,7,?: e11 28863 9:?: 10:8,9,?: e10 28869 qed:10:
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbc3orgVD

Proof of Theorem sbc3orgVD
StepHypRef Expression
1 idn1 28739 . . . . . 6
2 sbcorg 3208 . . . . . 6
31, 2e1_ 28802 . . . . 5
4 df-3or 938 . . . . . . . . 9
54bicomi 195 . . . . . . . 8
65ax-gen 1556 . . . . . . 7
7 spsbc 3175 . . . . . . 7
81, 6, 7e10 28869 . . . . . 6
9 sbcbig 3209 . . . . . . 7
109biimpd 200 . . . . . 6
111, 8, 10e11 28863 . . . . 5
12 bitr3 28667 . . . . . 6
1312com12 30 . . . . 5
143, 11, 13e11 28863 . . . 4
15 sbcorg 3208 . . . . . 6
161, 15e1_ 28802 . . . . 5
17 orbi1 688 . . . . 5
1816, 17e1_ 28802 . . . 4
19 bibi1 319 . . . . 5
2019biimprd 216 . . . 4
2114, 18, 20e11 28863 . . 3
22 df-3or 938 . . . 4
2322bicomi 195 . . 3
24 bibi1 319 . . . 4
2524biimprd 216 . . 3
2621, 23, 25e10 28869 . 2
2726in1 28736 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wo 359   w3o 936  wal 1550   wcel 1726  wsbc 3163 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164  df-vd1 28735
 Copyright terms: Public domain W3C validator