Theorem ssind 3837

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
ssind.1	|- ( ph -> A C_ B )
ssind.2	|- ( ph -> A C_ C )

Assertion

Ref	Expression
ssind	|- ( ph -> A C_ ( B i^i C ) )

Proof of Theorem ssind

Step	Hyp	Ref	Expression
1		ssind.1	. . 3 |- ( ph -> A C_ B )
2		ssind.2	. . 3 |- ( ph -> A C_ C )
3	1, 2	jca 554	. 2 |- ( ph -> ( A C_ B /\ A C_ C ) )
4		ssin 3835	. 2 |- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
5	3, 4	sylib 208	1 |- ( ph -> A C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 384   i^i cin 3573   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  mreexexlem3d  16306  isacs1i  16318  rescabs  16493  funcres2c  16561  lsmmod  18088  gsumzres  18310  gsumzsubmcl  18318  gsum2d  18371  issubdrg  18805  lspdisj  19125  mplind  19502  ntrin  20865  elcls  20877  neitr  20984  restcls  20985  lmss  21102  xkoinjcn  21490  trfg  21695  trust  22033  utoptop  22038  restutop  22041  isngp2  22401  lebnumii  22765  causs  23096  dvreslem  23673  c1lip3  23762  ssjo  28306  dmdbr5  29167  mdslj2i  29179  mdsl2bi  29182  mdslmd1lem2  29185  mdsymlem5  29266  difininv  29354  bnj1286  31087  mclsind  31467  neiin  32327  topmeet  32359  fnemeet2  32362  bj-restpw  33045  bj-restb  33047  bj-restuni2  33051  idresssidinxp  34079  pmod1i  35134  dihmeetlem1N  36579  dihglblem5apreN  36580  dochdmj1  36679  mapdin  36951  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  trrelind  37957  isotone2  38347  nzin  38517  inmap  39401  islptre  39851  limccog  39852  limcresiooub  39874  limcresioolb  39875  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  fourierdlem48  40371  fourierdlem49  40372  fourierdlem113  40436  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  sssmf  40947  smflimlem2  40980  smfsuplem1  41017  setrec2fun  42439