Theorem ssind 3572

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	. 2 |- ( ph -> A C_ B )
2		ssind.2	. 2 |- ( ph -> A C_ C )
3		ssin 3570	. . 3 |- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
4	3	biimpi 194	. 2 |- ( ( A C_ B /\ A C_ C ) -> A C_ ( B i^i C ) )
5	1, 2, 4	syl2anc 661	1 |- ( ph -> A C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   i^i cin 3325   C_ wss 3326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3333  df-ss 3340

This theorem is referenced by:  mreexexlem3d  14582  isacs1i  14593  rescabs  14744  funcres2c  14809  lsmmod  16170  gsumzres  16386  gsumzresOLD  16390  gsumzsubmcl  16400  gsumzsubmclOLD  16401  gsum2d  16461  gsum2dOLD  16462  issubdrg  16888  lspdisj  17204  mplind  17582  ntrin  18663  elcls  18675  neitr  18782  restcls  18783  lmss  18900  xkoinjcn  19258  trfg  19462  trust  19802  utoptop  19807  restutop  19810  isngp2  20187  lebnumii  20536  causs  20807  dvreslem  21382  c1lip3  21469  ssjo  24848  dmdbr5  25710  mdslj2i  25722  mdsl2bi  25725  mdslmd1lem2  25728  mdsymlem5  25809  neiin  28524  topmeet  28582  fnemeet2  28585  bnj1286  32007  pmod1i  33489  dihmeetlem1N  34932  dihglblem5apreN  34933  dochdmj1  35032  mapdin  35304  baerlem3lem2  35352  baerlem5alem2  35353  baerlem5blem2  35354