Theorem ssind 4182

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  frrlem12  8240  frrlem13  8241  mreexexlem3d  17603  isacs1i  17614  rescabs  17791  funcres2c  17861  lsmmod  19641  gsumzres  19875  gsumzsubmcl  19884  gsum2d  19938  issubdrg  20748  lspdisj  21115  mplind  22058  ntrin  23036  elcls  23048  neitr  23155  restcls  23156  lmss  23273  xkoinjcn  23662  trfg  23866  trust  24204  utoptop  24209  restutop  24212  isngp2  24572  lebnumii  24943  causs  25275  dvreslem  25886  c1lip3  25976  ssjo  31533  dmdbr5  32394  mdslj2i  32406  mdsl2bi  32409  mdslmd1lem2  32412  mdsymlem5  32493  difininv  32602  idlsrgmulrssin  33588  bnj1286  35177  mclsind  35768  neiin  36530  topmeet  36562  fnemeet2  36565  bj-elpwg  37375  bj-restpw  37420  bj-restb  37422  bj-restuni2  37426  idresssidinxp  38649  pmod1i  40308  dihmeetlem1N  41750  dihglblem5apreN  41751  dochdmj1  41850  mapdin  42122  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  trrelind  44110  isotone2  44494  nzin  44763  inmap  45656  islptre  46067  limccog  46068  limcresiooub  46088  limcresioolb  46089  limsupresxr  46212  liminfresxr  46213  liminfvalxr  46229  fourierdlem48  46600  fourierdlem49  46601  fourierdlem113  46665  pimiooltgt  47156  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  sssmf  47184  smflimlem2  47218  smfsuplem1  47257  iscnrm3llem2  49437  setrec2fun  50179