Theorem ssind 4190

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3897   ⊆ wss 3898

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  frrlem12  8233  frrlem13  8234  mreexexlem3d  17554  isacs1i  17565  rescabs  17742  funcres2c  17812  lsmmod  19589  gsumzres  19823  gsumzsubmcl  19832  gsum2d  19886  issubdrg  20697  lspdisj  21064  mplind  22006  ntrin  22977  elcls  22989  neitr  23096  restcls  23097  lmss  23214  xkoinjcn  23603  trfg  23807  trust  24145  utoptop  24150  restutop  24153  isngp2  24513  lebnumii  24893  causs  25226  dvreslem  25838  c1lip3  25932  ssjo  31429  dmdbr5  32290  mdslj2i  32302  mdsl2bi  32305  mdslmd1lem2  32308  mdsymlem5  32389  difininv  32499  idlsrgmulrssin  33485  bnj1286  35052  mclsind  35635  neiin  36397  topmeet  36429  fnemeet2  36432  bj-elpwg  37117  bj-restpw  37157  bj-restb  37159  bj-restuni2  37163  idresssidinxp  38367  pmod1i  39968  dihmeetlem1N  41410  dihglblem5apreN  41411  dochdmj1  41510  mapdin  41782  baerlem3lem2  41830  baerlem5alem2  41831  baerlem5blem2  41832  trrelind  43783  isotone2  44167  nzin  44436  inmap  45331  islptre  45744  limccog  45745  limcresiooub  45765  limcresioolb  45766  limsupresxr  45889  liminfresxr  45890  liminfvalxr  45906  fourierdlem48  46277  fourierdlem49  46278  fourierdlem113  46342  pimiooltgt  46833  pimdecfgtioc  46838  pimincfltioc  46839  pimdecfgtioo  46840  pimincfltioo  46841  sssmf  46861  smflimlem2  46895  smfsuplem1  46934  iscnrm3llem2  49075  setrec2fun  49818