Theorem ssind 4159

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

Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  mreexexlem3d  16909  isacs1i  16920  rescabs  17095  funcres2c  17163  lsmmod  18793  gsumzres  19022  gsumzsubmcl  19031  gsum2d  19085  issubdrg  19553  lspdisj  19890  mplind  20741  ntrin  21666  elcls  21678  neitr  21785  restcls  21786  lmss  21903  xkoinjcn  22292  trfg  22496  trust  22835  utoptop  22840  restutop  22843  isngp2  23203  lebnumii  23571  causs  23902  dvreslem  24512  c1lip3  24602  ssjo  29230  dmdbr5  30091  mdslj2i  30103  mdsl2bi  30106  mdslmd1lem2  30109  mdsymlem5  30190  difininv  30288  idlsrgmulrssin  31066  bnj1286  32401  mclsind  32930  frrlem12  33247  frrlem13  33248  neiin  33793  topmeet  33825  fnemeet2  33828  bj-elpwg  34469  bj-restpw  34507  bj-restb  34509  bj-restuni2  34513  idresssidinxp  35726  pmod1i  37144  dihmeetlem1N  38586  dihglblem5apreN  38587  dochdmj1  38686  mapdin  38958  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  trrelind  40366  isotone2  40752  nzin  41022  inmap  41838  islptre  42261  limccog  42262  limcresiooub  42284  limcresioolb  42285  limsupresxr  42408  liminfresxr  42409  liminfvalxr  42425  fourierdlem48  42796  fourierdlem49  42797  fourierdlem113  42861  pimiooltgt  43346  pimdecfgtioc  43350  pimincfltioc  43351  pimdecfgtioo  43352  pimincfltioo  43353  sssmf  43372  smflimlem2  43405  smfsuplem1  43442  setrec2fun  45222