Theorem ssind 4140

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  frrlem12  8343  frrlem13  8344  setrec2fun  10000  mreexexlem3d  17849  isacs1i  17860  rescabs  18037  funcres2c  18107  lsmmod  19919  gsumzres  20153  gsumzsubmcl  20162  gsum2d  20216  issubdrg  21067  lspdisj  21433  mplind  22409  ntrin  23409  elcls  23421  neitr  23528  restcls  23529  lmss  23646  xkoinjcn  24036  trfg  24240  trust  24578  utoptop  24583  restutop  24586  isngp2  24946  lebnumii  25317  causs  25649  dvreslem  26259  c1lip3  26349  ssjo  32079  dmdbr5  32940  mdslj2i  32952  mdsl2bi  32955  mdslmd1lem2  32958  mdsymlem5  33039  difininv  33185  idlsrgmulrssin  34115  bnj1286  35719  mclsind  36502  neiin  37298  topmeet  37330  fnemeet2  37333  bj-elpwg  38158  bj-restpw  38204  bj-restb  38206  bj-restuni2  38210  idresssidinxp  39438  pmod1i  41097  dihmeetlem1N  42539  dihglblem5apreN  42540  dochdmj1  42639  mapdin  42911  baerlem3lem2  42959  baerlem5alem2  42960  baerlem5blem2  42961  trrelind  44857  isotone2  45241  nzin  45494  inmap  46427  islptre  46836  limccog  46837  limcresiooub  46857  limcresioolb  46858  limsupresxr  46981  liminfresxr  46982  liminfvalxr  46998  fourierdlem48  47369  fourierdlem49  47370  fourierdlem113  47434  pimiooltgt  47925  pimdecfgtioc  47930  pimincfltioc  47931  pimdecfgtioo  47932  pimincfltioo  47933  sssmf  47953  smflimlem2  47987  smfsuplem1  48026  iscnrm3llem2  50269