Theorem ssind 4176

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

Syntax hints:   → wi 4   ∧ wa 396   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  frrlem12  8244  frrlem13  8245  mreexexlem3d  17610  isacs1i  17621  rescabs  17798  funcres2c  17868  lsmmod  19648  gsumzres  19882  gsumzsubmcl  19891  gsum2d  19945  issubdrg  20759  lspdisj  21125  mplind  22053  ntrin  23051  elcls  23063  neitr  23170  restcls  23171  lmss  23288  xkoinjcn  23677  trfg  23881  trust  24219  utoptop  24224  restutop  24227  isngp2  24587  lebnumii  24958  causs  25290  dvreslem  25901  c1lip3  25991  ssjo  31543  dmdbr5  32404  mdslj2i  32416  mdsl2bi  32419  mdslmd1lem2  32422  mdsymlem5  32503  difininv  32612  idlsrgmulrssin  33603  bnj1286  35208  mclsind  35805  neiin  36567  topmeet  36599  fnemeet2  36602  bj-elpwg  37412  bj-restpw  37457  bj-restb  37459  bj-restuni2  37463  idresssidinxp  38688  pmod1i  40347  dihmeetlem1N  41789  dihglblem5apreN  41790  dochdmj1  41889  mapdin  42161  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  trrelind  44116  isotone2  44500  nzin  44769  inmap  45661  islptre  46071  limccog  46072  limcresiooub  46092  limcresioolb  46093  limsupresxr  46216  liminfresxr  46217  liminfvalxr  46233  fourierdlem48  46604  fourierdlem49  46605  fourierdlem113  46669  pimiooltgt  47160  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  sssmf  47188  smflimlem2  47222  smfsuplem1  47261  iscnrm3llem2  49447  setrec2fun  50189