Theorem ssind 3722

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 3720	. . 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 3475   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490

This theorem is referenced by:  mreexexlem3d  14894  isacs1i  14905  rescabs  15056  funcres2c  15121  lsmmod  16486  gsumzres  16702  gsumzresOLD  16706  gsumzsubmcl  16716  gsumzsubmclOLD  16717  gsum2d  16787  gsum2dOLD  16788  issubdrg  17234  lspdisj  17551  mplind  17935  ntrin  19325  elcls  19337  neitr  19444  restcls  19445  lmss  19562  xkoinjcn  19920  trfg  20124  trust  20464  utoptop  20469  restutop  20472  isngp2  20849  lebnumii  21198  causs  21469  dvreslem  22045  c1lip3  22132  ssjo  26038  dmdbr5  26900  mdslj2i  26912  mdsl2bi  26915  mdslmd1lem2  26918  mdsymlem5  26999  neiin  29725  topmeet  29783  fnemeet2  29786  nzin  30823  islptre  31161  limcresiooub  31184  fourierdlem48  31455  fourierdlem49  31456  fourierdlem113  31520  bnj1286  33154  pmod1i  34644  dihmeetlem1N  36087  dihglblem5apreN  36088  dochdmj1  36187  mapdin  36459  baerlem3lem2  36507  baerlem5alem2  36508  baerlem5blem2  36509  trrelind  36788