Theorem ssind 4195

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3902   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  frrlem12  8249  frrlem13  8250  mreexexlem3d  17581  isacs1i  17592  rescabs  17769  funcres2c  17839  lsmmod  19616  gsumzres  19850  gsumzsubmcl  19859  gsum2d  19913  issubdrg  20725  lspdisj  21092  mplind  22037  ntrin  23017  elcls  23029  neitr  23136  restcls  23137  lmss  23254  xkoinjcn  23643  trfg  23847  trust  24185  utoptop  24190  restutop  24193  isngp2  24553  lebnumii  24933  causs  25266  dvreslem  25878  c1lip3  25972  ssjo  31534  dmdbr5  32395  mdslj2i  32407  mdsl2bi  32410  mdslmd1lem2  32413  mdsymlem5  32494  difininv  32603  idlsrgmulrssin  33605  bnj1286  35194  mclsind  35783  neiin  36545  topmeet  36577  fnemeet2  36580  bj-elpwg  37297  bj-restpw  37342  bj-restb  37344  bj-restuni2  37348  idresssidinxp  38562  pmod1i  40221  dihmeetlem1N  41663  dihglblem5apreN  41664  dochdmj1  41763  mapdin  42035  baerlem3lem2  42083  baerlem5alem2  42084  baerlem5blem2  42085  trrelind  44018  isotone2  44402  nzin  44671  inmap  45564  islptre  45976  limccog  45977  limcresiooub  45997  limcresioolb  45998  limsupresxr  46121  liminfresxr  46122  liminfvalxr  46138  fourierdlem48  46509  fourierdlem49  46510  fourierdlem113  46574  pimiooltgt  47065  pimdecfgtioc  47070  pimincfltioc  47071  pimdecfgtioo  47072  pimincfltioo  47073  sssmf  47093  smflimlem2  47127  smfsuplem1  47166  iscnrm3llem2  49306  setrec2fun  50048