Theorem ssind 4194

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3904   ⊆ wss 3905

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  frrlem12  8237  frrlem13  8238  mreexexlem3d  17570  isacs1i  17581  rescabs  17758  funcres2c  17828  lsmmod  19572  gsumzres  19806  gsumzsubmcl  19815  gsum2d  19869  issubdrg  20683  lspdisj  21050  mplind  21993  ntrin  22964  elcls  22976  neitr  23083  restcls  23084  lmss  23201  xkoinjcn  23590  trfg  23794  trust  24133  utoptop  24138  restutop  24141  isngp2  24501  lebnumii  24881  causs  25214  dvreslem  25826  c1lip3  25920  ssjo  31409  dmdbr5  32270  mdslj2i  32282  mdsl2bi  32285  mdslmd1lem2  32288  mdsymlem5  32369  difininv  32479  idlsrgmulrssin  33460  bnj1286  34985  mclsind  35542  neiin  36305  topmeet  36337  fnemeet2  36340  bj-elpwg  37025  bj-restpw  37065  bj-restb  37067  bj-restuni2  37071  idresssidinxp  38281  pmod1i  39827  dihmeetlem1N  41269  dihglblem5apreN  41270  dochdmj1  41369  mapdin  41641  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  trrelind  43638  isotone2  44022  nzin  44291  inmap  45187  islptre  45601  limccog  45602  limcresiooub  45624  limcresioolb  45625  limsupresxr  45748  liminfresxr  45749  liminfvalxr  45765  fourierdlem48  46136  fourierdlem49  46137  fourierdlem113  46201  pimiooltgt  46692  pimdecfgtioc  46697  pimincfltioc  46698  pimdecfgtioo  46699  pimincfltioo  46700  sssmf  46720  smflimlem2  46754  smfsuplem1  46793  iscnrm3llem2  48935  setrec2fun  49678