Theorem ssind 4189

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

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

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  frrlem12  8300  frrlem13  8301  mreexexlem3d  17740  isacs1i  17751  rescabs  17928  funcres2c  17998  lsmmod  19808  gsumzres  20042  gsumzsubmcl  20051  gsum2d  20105  issubdrg  20952  lspdisj  21318  mplind  22292  ntrin  23292  elcls  23304  neitr  23411  restcls  23412  lmss  23529  xkoinjcn  23919  trfg  24123  trust  24461  utoptop  24466  restutop  24469  isngp2  24829  lebnumii  25200  causs  25532  dvreslem  26143  c1lip3  26233  ssjo  31936  dmdbr5  32797  mdslj2i  32809  mdsl2bi  32812  mdslmd1lem2  32815  mdsymlem5  32896  difininv  33000  idlsrgmulrssin  33931  bnj1286  35536  mclsind  36157  neiin  36959  topmeet  36991  fnemeet2  36994  bj-elpwg  37804  bj-restpw  37850  bj-restb  37852  bj-restuni2  37856  idresssidinxp  39070  pmod1i  40729  dihmeetlem1N  42171  dihglblem5apreN  42172  dochdmj1  42271  mapdin  42543  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  trrelind  44513  isotone2  44897  nzin  45150  inmap  46047  islptre  46457  limccog  46458  limcresiooub  46478  limcresioolb  46479  limsupresxr  46602  liminfresxr  46603  liminfvalxr  46619  fourierdlem48  46990  fourierdlem49  46991  fourierdlem113  47055  pimiooltgt  47546  pimdecfgtioc  47551  pimincfltioc  47552  pimdecfgtioo  47553  pimincfltioo  47554  sssmf  47574  smflimlem2  47608  smfsuplem1  47647  iscnrm3llem2  49884  setrec2fun  50626