Theorem ssind 4193

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  frrlem12  8239  frrlem13  8240  mreexexlem3d  17569  isacs1i  17580  rescabs  17757  funcres2c  17827  lsmmod  19604  gsumzres  19838  gsumzsubmcl  19847  gsum2d  19901  issubdrg  20713  lspdisj  21080  mplind  22025  ntrin  23005  elcls  23017  neitr  23124  restcls  23125  lmss  23242  xkoinjcn  23631  trfg  23835  trust  24173  utoptop  24178  restutop  24181  isngp2  24541  lebnumii  24921  causs  25254  dvreslem  25866  c1lip3  25960  ssjo  31522  dmdbr5  32383  mdslj2i  32395  mdsl2bi  32398  mdslmd1lem2  32401  mdsymlem5  32482  difininv  32592  idlsrgmulrssin  33594  bnj1286  35175  mclsind  35764  neiin  36526  topmeet  36558  fnemeet2  36561  bj-elpwg  37253  bj-restpw  37293  bj-restb  37295  bj-restuni2  37299  idresssidinxp  38503  pmod1i  40104  dihmeetlem1N  41546  dihglblem5apreN  41547  dochdmj1  41646  mapdin  41918  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  trrelind  43902  isotone2  44286  nzin  44555  inmap  45449  islptre  45861  limccog  45862  limcresiooub  45882  limcresioolb  45883  limsupresxr  46006  liminfresxr  46007  liminfvalxr  46023  fourierdlem48  46394  fourierdlem49  46395  fourierdlem113  46459  pimiooltgt  46950  pimdecfgtioc  46955  pimincfltioc  46956  pimdecfgtioo  46957  pimincfltioo  46958  sssmf  46978  smflimlem2  47012  smfsuplem1  47051  iscnrm3llem2  49191  setrec2fun  49933