Theorem sbcimg 3211

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 3173	. 2
2		dfsbcq2 3173	. . 3
3		dfsbcq2 3173	. . 3
4	2, 3	imbi12d 313	. 2
5		sbim 2140	. 2
6	1, 4, 5	vtoclbg 3021	1

Syntax hints:  ->wi 4  <->wb 178  =wceq 1654  [wsb 1660  e.wcel 1728  [.wsbc 3170

This theorem is referenced by:  sbcim1  3218  sbceqal  3224  sbcimdvOLD  3238  sbc19.21g  3241  sbcssg  3764  tfinds2  4884  iota4an  5483  riotass2  6626  sbcfung  28142  sbcim2g  28862  sbcssOLD  28866  onfrALTlem5  28867  sbcim2gVD  29228  sbcssgVD  29236  onfrALTlem5VD  29238  bnj538  29349  bnj110  29470  bnj92  29474  bnj539  29503  bnj540  29504  cdlemkid3N  31970  cdlemkid4  31971  cdlemk35s  31974  cdlemk39s  31976  cdlemk42  31978

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 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424

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 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-sbc 3171