Theorem ssind 4241

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	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
ssind.2	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Assertion

Ref	Expression
ssind	⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Proof of Theorem ssind

Step	Hyp	Ref	Expression
1		ssind.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssind.2	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶))
4		ssin 4239	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	sylib 218	1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3950   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  frrlem12  8322  frrlem13  8323  mreexexlem3d  17689  isacs1i  17700  rescabs  17877  rescabsOLD  17878  funcres2c  17948  lsmmod  19693  gsumzres  19927  gsumzsubmcl  19936  gsum2d  19990  issubdrg  20781  lspdisj  21127  mplind  22094  ntrin  23069  elcls  23081  neitr  23188  restcls  23189  lmss  23306  xkoinjcn  23695  trfg  23899  trust  24238  utoptop  24243  restutop  24246  isngp2  24610  lebnumii  24998  causs  25332  dvreslem  25944  c1lip3  26038  ssjo  31466  dmdbr5  32327  mdslj2i  32339  mdsl2bi  32342  mdslmd1lem2  32345  mdsymlem5  32426  difininv  32536  idlsrgmulrssin  33541  bnj1286  35033  mclsind  35575  neiin  36333  topmeet  36365  fnemeet2  36368  bj-elpwg  37053  bj-restpw  37093  bj-restb  37095  bj-restuni2  37099  idresssidinxp  38309  pmod1i  39850  dihmeetlem1N  41292  dihglblem5apreN  41293  dochdmj1  41392  mapdin  41664  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  trrelind  43678  isotone2  44062  nzin  44337  inmap  45214  islptre  45634  limccog  45635  limcresiooub  45657  limcresioolb  45658  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  fourierdlem48  46169  fourierdlem49  46170  fourierdlem113  46234  pimiooltgt  46725  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  sssmf  46753  smflimlem2  46787  smfsuplem1  46826  iscnrm3llem2  48847  setrec2fun  49211