Theorem ssind 4163

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  frrlem12  8084  frrlem13  8085  mreexexlem3d  17272  isacs1i  17283  rescabs  17464  funcres2c  17533  lsmmod  19196  gsumzres  19425  gsumzsubmcl  19434  gsum2d  19488  issubdrg  19964  lspdisj  20302  mplind  21188  ntrin  22120  elcls  22132  neitr  22239  restcls  22240  lmss  22357  xkoinjcn  22746  trfg  22950  trust  23289  utoptop  23294  restutop  23297  isngp2  23659  lebnumii  24035  causs  24367  dvreslem  24978  c1lip3  25068  ssjo  29710  dmdbr5  30571  mdslj2i  30583  mdsl2bi  30586  mdslmd1lem2  30589  mdsymlem5  30670  difininv  30765  idlsrgmulrssin  31560  bnj1286  32899  mclsind  33432  neiin  34448  topmeet  34480  fnemeet2  34483  bj-elpwg  35152  bj-restpw  35190  bj-restb  35192  bj-restuni2  35196  idresssidinxp  36371  pmod1i  37789  dihmeetlem1N  39231  dihglblem5apreN  39232  dochdmj1  39331  mapdin  39603  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  trrelind  41162  isotone2  41548  nzin  41825  inmap  42638  islptre  43050  limccog  43051  limcresiooub  43073  limcresioolb  43074  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  fourierdlem48  43585  fourierdlem49  43586  fourierdlem113  43650  pimiooltgt  44135  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  sssmf  44161  smflimlem2  44194  smfsuplem1  44231  iscnrm3llem2  46132  setrec2fun  46284