Theorem ssind 4186

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∩ cin 3898   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  frrlem12  8299  frrlem13  8300  setrec2fun  9954  mreexexlem3d  17800  isacs1i  17811  rescabs  17988  funcres2c  18058  lsmmod  19869  gsumzres  20103  gsumzsubmcl  20112  gsum2d  20166  issubdrg  21017  lspdisj  21383  mplind  22359  ntrin  23359  elcls  23371  neitr  23478  restcls  23479  lmss  23596  xkoinjcn  23986  trfg  24190  trust  24528  utoptop  24533  restutop  24536  isngp2  24896  lebnumii  25267  causs  25599  dvreslem  26209  c1lip3  26299  ssjo  32031  dmdbr5  32892  mdslj2i  32904  mdsl2bi  32907  mdslmd1lem2  32910  mdsymlem5  32991  difininv  33095  idlsrgmulrssin  34027  bnj1286  35632  mclsind  36304  neiin  37090  topmeet  37122  fnemeet2  37125  bj-elpwg  37935  bj-restpw  37981  bj-restb  37983  bj-restuni2  37987  idresssidinxp  39214  pmod1i  40873  dihmeetlem1N  42315  dihglblem5apreN  42316  dochdmj1  42415  mapdin  42687  baerlem3lem2  42735  baerlem5alem2  42736  baerlem5blem2  42737  trrelind  44624  isotone2  45008  nzin  45261  inmap  46165  islptre  46575  limccog  46576  limcresiooub  46596  limcresioolb  46597  limsupresxr  46720  liminfresxr  46721  liminfvalxr  46737  fourierdlem48  47108  fourierdlem49  47109  fourierdlem113  47173  pimiooltgt  47664  pimdecfgtioc  47669  pimincfltioc  47670  pimdecfgtioo  47671  pimincfltioo  47672  sssmf  47692  smflimlem2  47726  smfsuplem1  47765  iscnrm3llem2  50002