Theorem ssind 4181

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  frrlem12  8247  frrlem13  8248  mreexexlem3d  17612  isacs1i  17623  rescabs  17800  funcres2c  17870  lsmmod  19650  gsumzres  19884  gsumzsubmcl  19893  gsum2d  19947  issubdrg  20757  lspdisj  21123  mplind  22048  ntrin  23026  elcls  23038  neitr  23145  restcls  23146  lmss  23263  xkoinjcn  23652  trfg  23856  trust  24194  utoptop  24199  restutop  24202  isngp2  24562  lebnumii  24933  causs  25265  dvreslem  25876  c1lip3  25966  ssjo  31518  dmdbr5  32379  mdslj2i  32391  mdsl2bi  32394  mdslmd1lem2  32397  mdsymlem5  32478  difininv  32587  idlsrgmulrssin  33573  bnj1286  35161  mclsind  35752  neiin  36514  topmeet  36546  fnemeet2  36549  bj-elpwg  37359  bj-restpw  37404  bj-restb  37406  bj-restuni2  37410  idresssidinxp  38635  pmod1i  40294  dihmeetlem1N  41736  dihglblem5apreN  41737  dochdmj1  41836  mapdin  42108  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  trrelind  44092  isotone2  44476  nzin  44745  inmap  45638  islptre  46049  limccog  46050  limcresiooub  46070  limcresioolb  46071  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  fourierdlem48  46582  fourierdlem49  46583  fourierdlem113  46647  pimiooltgt  47138  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  sssmf  47166  smflimlem2  47200  smfsuplem1  47239  iscnrm3llem2  49425  setrec2fun  50167