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

Syntax hints:   → wi 4   ∧ wa 400   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  frrlem12  8295  frrlem13  8296  mreexexlem3d  17703  isacs1i  17714  rescabs  17891  funcres2c  17961  lsmmod  19746  gsumzres  19980  gsumzsubmcl  19989  gsum2d  20043  issubdrg  20864  lspdisj  21230  mplind  22202  ntrin  23199  elcls  23211  neitr  23318  restcls  23319  lmss  23436  xkoinjcn  23825  trfg  24029  trust  24367  utoptop  24372  restutop  24375  isngp2  24735  lebnumii  25106  causs  25438  dvreslem  26049  c1lip3  26139  ssjo  31777  dmdbr5  32638  mdslj2i  32650  mdsl2bi  32653  mdslmd1lem2  32656  mdsymlem5  32737  difininv  32841  idlsrgmulrssin  33781  bnj1286  35385  mclsind  36040  neiin  36821  topmeet  36853  fnemeet2  36856  bj-elpwg  37666  bj-restpw  37712  bj-restb  37714  bj-restuni2  37718  idresssidinxp  38941  pmod1i  40600  dihmeetlem1N  42042  dihglblem5apreN  42043  dochdmj1  42142  mapdin  42414  baerlem3lem2  42462  baerlem5alem2  42463  baerlem5blem2  42464  trrelind  44371  isotone2  44755  nzin  45008  inmap  45905  islptre  46315  limccog  46316  limcresiooub  46336  limcresioolb  46337  limsupresxr  46460  liminfresxr  46461  liminfvalxr  46477  fourierdlem48  46848  fourierdlem49  46849  fourierdlem113  46913  pimiooltgt  47404  pimdecfgtioc  47409  pimincfltioc  47410  pimdecfgtioo  47411  pimincfltioo  47412  sssmf  47432  smflimlem2  47466  smfsuplem1  47505  iscnrm3llem2  49705  setrec2fun  50447