Theorem ssind 4233

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

Syntax hints:   → wi 4   ∧ wa 397   ∩ cin 3948   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  frrlem12  8282  frrlem13  8283  mreexexlem3d  17590  isacs1i  17601  rescabs  17782  rescabsOLD  17783  funcres2c  17852  lsmmod  19543  gsumzres  19777  gsumzsubmcl  19786  gsum2d  19840  issubdrg  20401  lspdisj  20738  mplind  21631  ntrin  22565  elcls  22577  neitr  22684  restcls  22685  lmss  22802  xkoinjcn  23191  trfg  23395  trust  23734  utoptop  23739  restutop  23742  isngp2  24106  lebnumii  24482  causs  24815  dvreslem  25426  c1lip3  25516  ssjo  30700  dmdbr5  31561  mdslj2i  31573  mdsl2bi  31576  mdslmd1lem2  31579  mdsymlem5  31660  difininv  31755  idlsrgmulrssin  32627  bnj1286  34030  mclsind  34561  neiin  35217  topmeet  35249  fnemeet2  35252  bj-elpwg  35933  bj-restpw  35973  bj-restb  35975  bj-restuni2  35979  idresssidinxp  37177  pmod1i  38719  dihmeetlem1N  40161  dihglblem5apreN  40162  dochdmj1  40261  mapdin  40533  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  trrelind  42416  isotone2  42800  nzin  43077  inmap  43908  islptre  44335  limccog  44336  limcresiooub  44358  limcresioolb  44359  limsupresxr  44482  liminfresxr  44483  liminfvalxr  44499  fourierdlem48  44870  fourierdlem49  44871  fourierdlem113  44935  pimiooltgt  45426  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  sssmf  45454  smflimlem2  45488  smfsuplem1  45527  iscnrm3llem2  47583  setrec2fun  47737