Theorem ssind 4207

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3916   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  frrlem12  8279  frrlem13  8280  mreexexlem3d  17614  isacs1i  17625  rescabs  17802  funcres2c  17872  lsmmod  19612  gsumzres  19846  gsumzsubmcl  19855  gsum2d  19909  issubdrg  20696  lspdisj  21042  mplind  21984  ntrin  22955  elcls  22967  neitr  23074  restcls  23075  lmss  23192  xkoinjcn  23581  trfg  23785  trust  24124  utoptop  24129  restutop  24132  isngp2  24492  lebnumii  24872  causs  25205  dvreslem  25817  c1lip3  25911  ssjo  31383  dmdbr5  32244  mdslj2i  32256  mdsl2bi  32259  mdslmd1lem2  32262  mdsymlem5  32343  difininv  32453  idlsrgmulrssin  33491  bnj1286  35016  mclsind  35564  neiin  36327  topmeet  36359  fnemeet2  36362  bj-elpwg  37047  bj-restpw  37087  bj-restb  37089  bj-restuni2  37093  idresssidinxp  38303  pmod1i  39849  dihmeetlem1N  41291  dihglblem5apreN  41292  dochdmj1  41391  mapdin  41663  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  trrelind  43661  isotone2  44045  nzin  44314  inmap  45210  islptre  45624  limccog  45625  limcresiooub  45647  limcresioolb  45648  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  fourierdlem48  46159  fourierdlem49  46160  fourierdlem113  46224  pimiooltgt  46715  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  sssmf  46743  smflimlem2  46777  smfsuplem1  46816  iscnrm3llem2  48942  setrec2fun  49685