Theorem ssind 4248

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  frrlem12  8320  frrlem13  8321  mreexexlem3d  17690  isacs1i  17701  rescabs  17882  rescabsOLD  17883  funcres2c  17954  lsmmod  19707  gsumzres  19941  gsumzsubmcl  19950  gsum2d  20004  issubdrg  20797  lspdisj  21144  mplind  22111  ntrin  23084  elcls  23096  neitr  23203  restcls  23204  lmss  23321  xkoinjcn  23710  trfg  23914  trust  24253  utoptop  24258  restutop  24261  isngp2  24625  lebnumii  25011  causs  25345  dvreslem  25958  c1lip3  26052  ssjo  31475  dmdbr5  32336  mdslj2i  32348  mdsl2bi  32351  mdslmd1lem2  32354  mdsymlem5  32435  difininv  32544  idlsrgmulrssin  33520  bnj1286  35011  mclsind  35554  neiin  36314  topmeet  36346  fnemeet2  36349  bj-elpwg  37034  bj-restpw  37074  bj-restb  37076  bj-restuni2  37080  idresssidinxp  38289  pmod1i  39830  dihmeetlem1N  41272  dihglblem5apreN  41273  dochdmj1  41372  mapdin  41644  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  trrelind  43654  isotone2  44038  nzin  44313  inmap  45151  islptre  45574  limccog  45575  limcresiooub  45597  limcresioolb  45598  limsupresxr  45721  liminfresxr  45722  liminfvalxr  45738  fourierdlem48  46109  fourierdlem49  46110  fourierdlem113  46174  pimiooltgt  46665  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  sssmf  46693  smflimlem2  46727  smfsuplem1  46766  iscnrm3llem2  48746  setrec2fun  48922