Theorem ssind 4211

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

Syntax hints:   → wi 4   ∧ wa 398   ∩ cin 3937   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954

This theorem is referenced by:  mreexexlem3d  16919  isacs1i  16930  rescabs  17105  funcres2c  17173  lsmmod  18803  gsumzres  19031  gsumzsubmcl  19040  gsum2d  19094  issubdrg  19562  lspdisj  19899  mplind  20284  ntrin  21671  elcls  21683  neitr  21790  restcls  21791  lmss  21908  xkoinjcn  22297  trfg  22501  trust  22840  utoptop  22845  restutop  22848  isngp2  23208  lebnumii  23572  causs  23903  dvreslem  24509  c1lip3  24598  ssjo  29226  dmdbr5  30087  mdslj2i  30099  mdsl2bi  30102  mdslmd1lem2  30105  mdsymlem5  30186  difininv  30281  bnj1286  32293  mclsind  32819  frrlem12  33136  frrlem13  33137  neiin  33682  topmeet  33714  fnemeet2  33717  bj-elpwg  34347  bj-restpw  34385  bj-restb  34387  bj-restuni2  34391  idresssidinxp  35568  pmod1i  36986  dihmeetlem1N  38428  dihglblem5apreN  38429  dochdmj1  38528  mapdin  38800  baerlem3lem2  38848  baerlem5alem2  38849  baerlem5blem2  38850  trrelind  40017  isotone2  40406  nzin  40657  inmap  41479  islptre  41907  limccog  41908  limcresiooub  41930  limcresioolb  41931  limsupresxr  42054  liminfresxr  42055  liminfvalxr  42071  fourierdlem48  42446  fourierdlem49  42447  fourierdlem113  42511  pimiooltgt  42996  pimdecfgtioc  43000  pimincfltioc  43001  pimdecfgtioo  43002  pimincfltioo  43003  sssmf  43022  smflimlem2  43055  smfsuplem1  43092  setrec2fun  44802