Theorem ssind 4196

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∩ cin 3907   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925

This theorem is used by:  frrlem12  8303  frrlem13  8304  mreexexlem3d  17727  isacs1i  17738  rescabs  17915  funcres2c  17985  lsmmod  19776  gsumzres  20010  gsumzsubmcl  20019  gsum2d  20073  issubdrg  20920  lspdisj  21286  mplind  22258  ntrin  23255  elcls  23267  neitr  23374  restcls  23375  lmss  23492  xkoinjcn  23881  trfg  24085  trust  24423  utoptop  24428  restutop  24431  isngp2  24791  lebnumii  25162  causs  25494  dvreslem  26105  c1lip3  26195  ssjo  31836  dmdbr5  32697  mdslj2i  32709  mdsl2bi  32712  mdslmd1lem2  32715  mdsymlem5  32796  difininv  32900  idlsrgmulrssin  33834  bnj1286  35439  mclsind  36083  neiin  36884  topmeet  36916  fnemeet2  36919  bj-elpwg  37729  bj-restpw  37775  bj-restb  37777  bj-restuni2  37781  idresssidinxp  39004  pmod1i  40663  dihmeetlem1N  42105  dihglblem5apreN  42106  dochdmj1  42205  mapdin  42477  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  trrelind  44432  isotone2  44816  nzin  45069  inmap  45966  islptre  46376  limccog  46377  limcresiooub  46397  limcresioolb  46398  limsupresxr  46521  liminfresxr  46522  liminfvalxr  46538  fourierdlem48  46909  fourierdlem49  46910  fourierdlem113  46974  pimiooltgt  47465  pimdecfgtioc  47470  pimincfltioc  47471  pimdecfgtioo  47472  pimincfltioo  47473  sssmf  47493  smflimlem2  47527  smfsuplem1  47566  iscnrm3llem2  49769  setrec2fun  50511