Theorem ssind 4191

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

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3901   ⊆ wss 3902

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3909  df-ss 3919

This theorem is referenced by:  frrlem12  8227  frrlem13  8228  mreexexlem3d  17552  isacs1i  17563  rescabs  17740  funcres2c  17810  lsmmod  19588  gsumzres  19822  gsumzsubmcl  19831  gsum2d  19885  issubdrg  20696  lspdisj  21063  mplind  22006  ntrin  22977  elcls  22989  neitr  23096  restcls  23097  lmss  23214  xkoinjcn  23603  trfg  23807  trust  24145  utoptop  24150  restutop  24153  isngp2  24513  lebnumii  24893  causs  25226  dvreslem  25838  c1lip3  25932  ssjo  31425  dmdbr5  32286  mdslj2i  32298  mdsl2bi  32301  mdslmd1lem2  32304  mdsymlem5  32385  difininv  32495  idlsrgmulrssin  33476  bnj1286  35029  mclsind  35612  neiin  36372  topmeet  36404  fnemeet2  36407  bj-elpwg  37092  bj-restpw  37132  bj-restb  37134  bj-restuni2  37138  idresssidinxp  38348  pmod1i  39893  dihmeetlem1N  41335  dihglblem5apreN  41336  dochdmj1  41435  mapdin  41707  baerlem3lem2  41755  baerlem5alem2  41756  baerlem5blem2  41757  trrelind  43704  isotone2  44088  nzin  44357  inmap  45252  islptre  45665  limccog  45666  limcresiooub  45686  limcresioolb  45687  limsupresxr  45810  liminfresxr  45811  liminfvalxr  45827  fourierdlem48  46198  fourierdlem49  46199  fourierdlem113  46263  pimiooltgt  46754  pimdecfgtioc  46759  pimincfltioc  46760  pimdecfgtioo  46761  pimincfltioo  46762  sssmf  46782  smflimlem2  46816  smfsuplem1  46855  iscnrm3llem2  48987  setrec2fun  49730