Theorem sbcimg 3253

Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)

Assertion

Ref	Expression
sbcimg

Proof of Theorem sbcimg

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3215	. 2
2		dfsbcq2 3215	. . 3
3		dfsbcq2 3215	. . 3
4	2, 3	imbi12d 313	. 2
5		sbim 2137	. 2
6	1, 4, 5	vtoclbg 3062	1

Syntax hints:  ->wi 4  <->wb 178  =wceq 1662  [wsb 1668  e.wcel 1724  [.wsbc 3212

This theorem is referenced by:  sbcim1  3260  sbceqal  3267  sbcimdvOLD  3281  sbc19.21g  3284  sbcssg  3811  iota4an  5399  sbcfung  5440  riotass2  6054  tfinds2  6439  sbcim2g  29814  sbcssOLD  29818  onfrALTlem5  29819  sbcim2gVD  30180  sbcssgVD  30188  onfrALTlem5VD  30190  bnj538  30301  bnj110  30422  bnj92  30426  bnj539  30455  bnj540  30456  cdlemkid3N  33003  cdlemkid4  33004  cdlemk35s  33007  cdlemk39s  33009  cdlemk42  33011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-v 3008  df-sbc 3213