Theorem sbcimg 3265

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 3227	. 2
2		dfsbcq2 3227	. . 3
3		dfsbcq2 3227	. . 3
4	2, 3	imbi12d 313	. 2
5		sbim 2145	. 2
6	1, 4, 5	vtoclbg 3071	1

Syntax hints:  ->wi 4  <->wb 178  =wceq 1670  [wsb 1676  e.wcel 1732  [.wsbc 3224

This theorem is referenced by:  sbcim1  3272  sbceqal  3279  sbcimdvOLD  3293  sbc19.21g  3296  sbcssg  3824  iota4an  5420  sbcfung  5461  riotass2  6090  tfinds2  6484  sbcim2g  30091  sbcssOLD  30095  onfrALTlem5  30096  sbcim2gVD  30457  sbcssgVD  30465  onfrALTlem5VD  30467  bnj538  30578  bnj110  30699  bnj92  30703  bnj539  30732  bnj540  30733  cdlemkid3N  33280  cdlemkid4  33281  cdlemk35s  33284  cdlemk39s  33286  cdlemk42  33288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-sbc 3225