Theorem ssind 4201

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

Syntax hints:   → wi 4   ∧ wa 400   ∩ cin 3912   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920  df-ss 3930

This theorem is referenced by:  frrlem12  8294  frrlem13  8295  mreexexlem3d  17702  isacs1i  17713  rescabs  17890  funcres2c  17960  lsmmod  19745  gsumzres  19979  gsumzsubmcl  19988  gsum2d  20042  issubdrg  20861  lspdisj  21227  mplind  22190  ntrin  23187  elcls  23199  neitr  23306  restcls  23307  lmss  23424  xkoinjcn  23813  trfg  24017  trust  24355  utoptop  24360  restutop  24363  isngp2  24723  lebnumii  25094  causs  25426  dvreslem  26037  c1lip3  26127  ssjo  31740  dmdbr5  32601  mdslj2i  32613  mdsl2bi  32616  mdslmd1lem2  32619  mdsymlem5  32700  difininv  32804  idlsrgmulrssin  33748  bnj1286  35352  mclsind  35995  neiin  36766  topmeet  36798  fnemeet2  36801  bj-elpwg  37610  bj-restpw  37656  bj-restb  37658  bj-restuni2  37662  idresssidinxp  38887  pmod1i  40546  dihmeetlem1N  41988  dihglblem5apreN  41989  dochdmj1  42088  mapdin  42360  baerlem3lem2  42408  baerlem5alem2  42409  baerlem5blem2  42410  trrelind  44317  isotone2  44701  nzin  44954  inmap  45851  islptre  46261  limccog  46262  limcresiooub  46282  limcresioolb  46283  limsupresxr  46406  liminfresxr  46407  liminfvalxr  46423  fourierdlem48  46794  fourierdlem49  46795  fourierdlem113  46859  pimiooltgt  47350  pimdecfgtioc  47355  pimincfltioc  47356  pimdecfgtioo  47357  pimincfltioo  47358  sssmf  47378  smflimlem2  47412  smfsuplem1  47451  iscnrm3llem2  49647  setrec2fun  50389