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

Theorem sbcim2g 28625
 Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3204. sbcim2g 28625 is sbcim2gVD 28989 without virtual deductions and was automatically derived from sbcim2gVD 28989 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbcim2g

Proof of Theorem sbcim2g
StepHypRef Expression
1 sbcimg 3204 . . . 4
21biimpd 200 . . 3
3 sbcimg 3204 . . 3
4 imbi2 316 . . . 4
54biimpcd 217 . . 3
62, 3, 5ee21 1385 . 2
7 idd 23 . . . 4
8 bi2 191 . . . 4
93, 7, 8ee13 28588 . . 3
109, 1sylibrd 227 . 2
116, 10impbid 185 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wcel 1726  wsbc 3163 This theorem is referenced by:  trsbc  28627  trsbcVD  28991 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-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
 Copyright terms: Public domain W3C validator