Theorem ssind 4204

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3913   ⊆ wss 3914

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 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  frrlem12  8276  frrlem13  8277  mreexexlem3d  17607  isacs1i  17618  rescabs  17795  funcres2c  17865  lsmmod  19605  gsumzres  19839  gsumzsubmcl  19848  gsum2d  19902  issubdrg  20689  lspdisj  21035  mplind  21977  ntrin  22948  elcls  22960  neitr  23067  restcls  23068  lmss  23185  xkoinjcn  23574  trfg  23778  trust  24117  utoptop  24122  restutop  24125  isngp2  24485  lebnumii  24865  causs  25198  dvreslem  25810  c1lip3  25904  ssjo  31376  dmdbr5  32237  mdslj2i  32249  mdsl2bi  32252  mdslmd1lem2  32255  mdsymlem5  32336  difininv  32446  idlsrgmulrssin  33484  bnj1286  35009  mclsind  35557  neiin  36320  topmeet  36352  fnemeet2  36355  bj-elpwg  37040  bj-restpw  37080  bj-restb  37082  bj-restuni2  37086  idresssidinxp  38296  pmod1i  39842  dihmeetlem1N  41284  dihglblem5apreN  41285  dochdmj1  41384  mapdin  41656  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  trrelind  43654  isotone2  44038  nzin  44307  inmap  45203  islptre  45617  limccog  45618  limcresiooub  45640  limcresioolb  45641  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  fourierdlem48  46152  fourierdlem49  46153  fourierdlem113  46217  pimiooltgt  46708  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  sssmf  46736  smflimlem2  46770  smfsuplem1  46809  iscnrm3llem2  48938  setrec2fun  49681