Theorem ssind 4195

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

Syntax hints:   → wi 4   ∧ wa 400   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  frrlem12  8282  frrlem13  8283  mreexexlem3d  17692  isacs1i  17703  rescabs  17880  funcres2c  17950  lsmmod  19736  gsumzres  19970  gsumzsubmcl  19979  gsum2d  20033  issubdrg  20852  lspdisj  21218  mplind  22181  ntrin  23179  elcls  23191  neitr  23298  restcls  23299  lmss  23416  xkoinjcn  23805  trfg  24009  trust  24347  utoptop  24352  restutop  24355  isngp2  24715  lebnumii  25086  causs  25418  dvreslem  26029  c1lip3  26119  ssjo  31708  dmdbr5  32569  mdslj2i  32581  mdsl2bi  32584  mdslmd1lem2  32587  mdsymlem5  32668  difininv  32773  idlsrgmulrssin  33720  bnj1286  35324  mclsind  35933  neiin  36705  topmeet  36737  fnemeet2  36740  bj-elpwg  37549  bj-restpw  37594  bj-restb  37596  bj-restuni2  37600  idresssidinxp  38825  pmod1i  40484  dihmeetlem1N  41926  dihglblem5apreN  41927  dochdmj1  42026  mapdin  42298  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  trrelind  44253  isotone2  44637  nzin  44892  inmap  45783  islptre  46193  limccog  46194  limcresiooub  46214  limcresioolb  46215  limsupresxr  46338  liminfresxr  46339  liminfvalxr  46355  fourierdlem48  46726  fourierdlem49  46727  fourierdlem113  46791  pimiooltgt  47282  pimdecfgtioc  47287  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  sssmf  47310  smflimlem2  47344  smfsuplem1  47383  iscnrm3llem2  49579  setrec2fun  50321