Theorem ssind 4137

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  frrlem12  8318  frrlem13  8319  setrec2fun  9976  mreexexlem3d  17825  isacs1i  17836  rescabs  18013  funcres2c  18083  lsmmod  19894  gsumzres  20128  gsumzsubmcl  20137  gsum2d  20191  issubdrg  21042  lspdisj  21408  mplind  22384  ntrin  23384  elcls  23396  neitr  23503  restcls  23504  lmss  23621  xkoinjcn  24011  trfg  24215  trust  24553  utoptop  24558  restutop  24561  isngp2  24921  lebnumii  25292  causs  25624  dvreslem  26234  c1lip3  26324  ssjo  32054  dmdbr5  32915  mdslj2i  32927  mdsl2bi  32930  mdslmd1lem2  32933  mdsymlem5  33014  difininv  33160  idlsrgmulrssin  34091  bnj1286  35695  mclsind  36421  neiin  37212  topmeet  37244  fnemeet2  37247  bj-elpwg  38059  bj-restpw  38105  bj-restb  38107  bj-restuni2  38111  idresssidinxp  39339  pmod1i  40998  dihmeetlem1N  42440  dihglblem5apreN  42441  dochdmj1  42540  mapdin  42812  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  trrelind  44758  isotone2  45142  nzin  45395  inmap  46315  islptre  46724  limccog  46725  limcresiooub  46745  limcresioolb  46746  limsupresxr  46869  liminfresxr  46870  liminfvalxr  46886  fourierdlem48  47257  fourierdlem49  47258  fourierdlem113  47322  pimiooltgt  47813  pimdecfgtioc  47818  pimincfltioc  47819  pimdecfgtioo  47820  pimincfltioo  47821  sssmf  47841  smflimlem2  47875  smfsuplem1  47914  iscnrm3llem2  50157