Theorem ssind 4166

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

Syntax hints:   → wi 4   ∧ wa 396   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  frrlem12  8113  frrlem13  8114  mreexexlem3d  17355  isacs1i  17366  rescabs  17547  rescabsOLD  17548  funcres2c  17617  lsmmod  19281  gsumzres  19510  gsumzsubmcl  19519  gsum2d  19573  issubdrg  20049  lspdisj  20387  mplind  21278  ntrin  22212  elcls  22224  neitr  22331  restcls  22332  lmss  22449  xkoinjcn  22838  trfg  23042  trust  23381  utoptop  23386  restutop  23389  isngp2  23753  lebnumii  24129  causs  24462  dvreslem  25073  c1lip3  25163  ssjo  29809  dmdbr5  30670  mdslj2i  30682  mdsl2bi  30685  mdslmd1lem2  30688  mdsymlem5  30769  difininv  30864  idlsrgmulrssin  31658  bnj1286  32999  mclsind  33532  neiin  34521  topmeet  34553  fnemeet2  34556  bj-elpwg  35225  bj-restpw  35263  bj-restb  35265  bj-restuni2  35269  idresssidinxp  36444  pmod1i  37862  dihmeetlem1N  39304  dihglblem5apreN  39305  dochdmj1  39404  mapdin  39676  baerlem3lem2  39724  baerlem5alem2  39725  baerlem5blem2  39726  trrelind  41273  isotone2  41659  nzin  41936  inmap  42749  islptre  43160  limccog  43161  limcresiooub  43183  limcresioolb  43184  limsupresxr  43307  liminfresxr  43308  liminfvalxr  43324  fourierdlem48  43695  fourierdlem49  43696  fourierdlem113  43760  pimiooltgt  44247  pimdecfgtioc  44252  pimincfltioc  44253  pimdecfgtioo  44254  pimincfltioo  44255  sssmf  44274  smflimlem2  44307  smfsuplem1  44344  iscnrm3llem2  46244  setrec2fun  46398