Theorem ssind 3668

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 3666	. . 3 |- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
4	3	biimpi 199	. 2 |- ( ( A C_ B /\ A C_ C ) -> A C_ ( B i^i C ) )
5	1, 2, 4	syl2anc 671	1 |- ( ph -> A C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 375   i^i cin 3415   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430

This theorem is referenced by:  mreexexlem3d  15601  isacs1i  15612  rescabs  15787  funcres2c  15855  lsmmod  17374  gsumzres  17592  gsumzsubmcl  17600  gsum2d  17653  issubdrg  18082  lspdisj  18397  mplind  18774  ntrin  20125  elcls  20138  neitr  20245  restcls  20246  lmss  20363  xkoinjcn  20751  trfg  20955  trust  21293  utoptop  21298  restutop  21301  isngp2  21660  lebnumii  22046  causs  22317  dvreslem  22913  c1lip3  23000  ssjo  27149  dmdbr5  28010  mdslj2i  28022  mdsl2bi  28025  mdslmd1lem2  28028  mdsymlem5  28109  bnj1286  29877  mclsind  30257  neiin  31037  topmeet  31069  fnemeet2  31072  pmod1i  33458  dihmeetlem1N  34903  dihglblem5apreN  34904  dochdmj1  35003  mapdin  35275  baerlem3lem2  35323  baerlem5alem2  35324  baerlem5blem2  35325  trrelind  36302  nzin  36711  islptre  37737  limccog  37738  limcresiooub  37761  limcresioolb  37762  fourierdlem48  38056  fourierdlem49  38057  fourierdlem113  38121