Theorem ssind 4216

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3925   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  frrlem12  8296  frrlem13  8297  mreexexlem3d  17658  isacs1i  17669  rescabs  17846  funcres2c  17916  lsmmod  19656  gsumzres  19890  gsumzsubmcl  19899  gsum2d  19953  issubdrg  20740  lspdisj  21086  mplind  22028  ntrin  22999  elcls  23011  neitr  23118  restcls  23119  lmss  23236  xkoinjcn  23625  trfg  23829  trust  24168  utoptop  24173  restutop  24176  isngp2  24536  lebnumii  24916  causs  25250  dvreslem  25862  c1lip3  25956  ssjo  31428  dmdbr5  32289  mdslj2i  32301  mdsl2bi  32304  mdslmd1lem2  32307  mdsymlem5  32388  difininv  32498  idlsrgmulrssin  33528  bnj1286  35050  mclsind  35592  neiin  36350  topmeet  36382  fnemeet2  36385  bj-elpwg  37070  bj-restpw  37110  bj-restb  37112  bj-restuni2  37116  idresssidinxp  38326  pmod1i  39867  dihmeetlem1N  41309  dihglblem5apreN  41310  dochdmj1  41409  mapdin  41681  baerlem3lem2  41729  baerlem5alem2  41730  baerlem5blem2  41731  trrelind  43689  isotone2  44073  nzin  44342  inmap  45233  islptre  45648  limccog  45649  limcresiooub  45671  limcresioolb  45672  limsupresxr  45795  liminfresxr  45796  liminfvalxr  45812  fourierdlem48  46183  fourierdlem49  46184  fourierdlem113  46248  pimiooltgt  46739  pimdecfgtioc  46744  pimincfltioc  46745  pimdecfgtioo  46746  pimincfltioo  46747  sssmf  46767  smflimlem2  46801  smfsuplem1  46840  iscnrm3llem2  48924  setrec2fun  49556