Theorem ssind 4192

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-in 3906  df-ss 3916

This theorem is referenced by:  frrlem12  8236  frrlem13  8237  mreexexlem3d  17562  isacs1i  17573  rescabs  17750  funcres2c  17820  lsmmod  19597  gsumzres  19831  gsumzsubmcl  19840  gsum2d  19894  issubdrg  20705  lspdisj  21072  mplind  22015  ntrin  22986  elcls  22998  neitr  23105  restcls  23106  lmss  23223  xkoinjcn  23612  trfg  23816  trust  24154  utoptop  24159  restutop  24162  isngp2  24522  lebnumii  24902  causs  25235  dvreslem  25847  c1lip3  25941  ssjo  31438  dmdbr5  32299  mdslj2i  32311  mdsl2bi  32314  mdslmd1lem2  32317  mdsymlem5  32398  difininv  32508  idlsrgmulrssin  33489  bnj1286  35042  mclsind  35625  neiin  36387  topmeet  36419  fnemeet2  36422  bj-elpwg  37107  bj-restpw  37147  bj-restb  37149  bj-restuni2  37153  idresssidinxp  38356  pmod1i  39957  dihmeetlem1N  41399  dihglblem5apreN  41400  dochdmj1  41499  mapdin  41771  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  trrelind  43772  isotone2  44156  nzin  44425  inmap  45320  islptre  45733  limccog  45734  limcresiooub  45754  limcresioolb  45755  limsupresxr  45878  liminfresxr  45879  liminfvalxr  45895  fourierdlem48  46266  fourierdlem49  46267  fourierdlem113  46331  pimiooltgt  46822  pimdecfgtioc  46827  pimincfltioc  46828  pimdecfgtioo  46829  pimincfltioo  46830  sssmf  46850  smflimlem2  46884  smfsuplem1  46923  iscnrm3llem2  49064  setrec2fun  49807