Theorem ssind 4262

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  frrlem12  8338  frrlem13  8339  mreexexlem3d  17704  isacs1i  17715  rescabs  17896  rescabsOLD  17897  funcres2c  17968  lsmmod  19717  gsumzres  19951  gsumzsubmcl  19960  gsum2d  20014  issubdrg  20803  lspdisj  21150  mplind  22117  ntrin  23090  elcls  23102  neitr  23209  restcls  23210  lmss  23327  xkoinjcn  23716  trfg  23920  trust  24259  utoptop  24264  restutop  24267  isngp2  24631  lebnumii  25017  causs  25351  dvreslem  25964  c1lip3  26058  ssjo  31479  dmdbr5  32340  mdslj2i  32352  mdsl2bi  32355  mdslmd1lem2  32358  mdsymlem5  32439  difininv  32547  idlsrgmulrssin  33506  bnj1286  34995  mclsind  35538  neiin  36298  topmeet  36330  fnemeet2  36333  bj-elpwg  37018  bj-restpw  37058  bj-restb  37060  bj-restuni2  37064  idresssidinxp  38264  pmod1i  39805  dihmeetlem1N  41247  dihglblem5apreN  41248  dochdmj1  41347  mapdin  41619  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  trrelind  43627  isotone2  44011  nzin  44287  inmap  45116  islptre  45540  limccog  45541  limcresiooub  45563  limcresioolb  45564  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  fourierdlem48  46075  fourierdlem49  46076  fourierdlem113  46140  pimiooltgt  46631  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  sssmf  46659  smflimlem2  46693  smfsuplem1  46732  iscnrm3llem2  48630  setrec2fun  48784