Theorem ssind 3799

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

Syntax hints:   → wi 4   ∧ wa 383   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  mreexexlem3d  16129  isacs1i  16141  rescabs  16316  funcres2c  16384  lsmmod  17911  gsumzres  18133  gsumzsubmcl  18141  gsum2d  18194  issubdrg  18628  lspdisj  18946  mplind  19323  ntrin  20675  elcls  20687  neitr  20794  restcls  20795  lmss  20912  xkoinjcn  21300  trfg  21505  trust  21843  utoptop  21848  restutop  21851  isngp2  22211  lebnumii  22573  causs  22904  dvreslem  23479  c1lip3  23566  ssjo  27690  dmdbr5  28551  mdslj2i  28563  mdsl2bi  28566  mdslmd1lem2  28569  mdsymlem5  28650  bnj1286  30341  mclsind  30721  neiin  31497  topmeet  31529  fnemeet2  31532  bj-restpw  32226  bj-restb  32228  bj-restuni2  32232  pmod1i  34152  dihmeetlem1N  35597  dihglblem5apreN  35598  dochdmj1  35697  mapdin  35969  baerlem3lem2  36017  baerlem5alem2  36018  baerlem5blem2  36019  trrelind  36976  isotone2  37367  nzin  37539  inmap  38396  islptre  38686  limccog  38687  limcresiooub  38709  limcresioolb  38710  fourierdlem48  39047  fourierdlem49  39048  fourierdlem113  39112  pimiooltgt  39598  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  sssmf  39625  smflimlem2  39658  setrec2fun  42238