Theorem ssind 4192

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 519	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶))
4		ssin 4190	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	sylib 220	1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ss 3921

This theorem is referenced by:  frrlem12  8273  frrlem13  8274  mreexexlem3d  17661  isacs1i  17672  rescabs  17849  funcres2c  17919  lsmmod  19698  gsumzres  19932  gsumzsubmcl  19941  gsum2d  19995  issubdrg  20809  lspdisj  21175  mplind  22103  ntrin  23101  elcls  23113  neitr  23220  restcls  23221  lmss  23338  xkoinjcn  23727  trfg  23931  trust  24269  utoptop  24274  restutop  24277  isngp2  24637  lebnumii  25008  causs  25340  dvreslem  25951  c1lip3  26041  ssjo  31596  dmdbr5  32457  mdslj2i  32469  mdsl2bi  32472  mdslmd1lem2  32475  mdsymlem5  32556  difininv  32665  idlsrgmulrssin  33670  bnj1286  35278  mclsind  35884  neiin  36656  topmeet  36688  fnemeet2  36691  bj-elpwg  37501  bj-restpw  37546  bj-restb  37548  bj-restuni2  37552  idresssidinxp  38777  pmod1i  40436  dihmeetlem1N  41878  dihglblem5apreN  41879  dochdmj1  41978  mapdin  42250  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  trrelind  44205  isotone2  44589  nzin  44858  inmap  45749  islptre  46159  limccog  46160  limcresiooub  46180  limcresioolb  46181  limsupresxr  46304  liminfresxr  46305  liminfvalxr  46321  fourierdlem48  46692  fourierdlem49  46693  fourierdlem113  46757  pimiooltgt  47248  pimdecfgtioc  47253  pimincfltioc  47254  pimdecfgtioo  47255  pimincfltioo  47256  sssmf  47276  smflimlem2  47310  smfsuplem1  47349  iscnrm3llem2  49535  setrec2fun  50277