Theorem ssind 4209

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

Syntax hints:   → wi 4   ∧ wa 398   ∩ cin 3935   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  mreexexlem3d  16917  isacs1i  16928  rescabs  17103  funcres2c  17171  lsmmod  18801  gsumzres  19029  gsumzsubmcl  19038  gsum2d  19092  issubdrg  19560  lspdisj  19897  mplind  20282  ntrin  21669  elcls  21681  neitr  21788  restcls  21789  lmss  21906  xkoinjcn  22295  trfg  22499  trust  22838  utoptop  22843  restutop  22846  isngp2  23206  lebnumii  23570  causs  23901  dvreslem  24507  c1lip3  24596  ssjo  29224  dmdbr5  30085  mdslj2i  30097  mdsl2bi  30100  mdslmd1lem2  30103  mdsymlem5  30184  difininv  30279  bnj1286  32291  mclsind  32817  frrlem12  33134  frrlem13  33135  neiin  33680  topmeet  33712  fnemeet2  33715  bj-elpwg  34348  bj-restpw  34386  bj-restb  34388  bj-restuni2  34392  idresssidinxp  35581  pmod1i  36999  dihmeetlem1N  38441  dihglblem5apreN  38442  dochdmj1  38541  mapdin  38813  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  trrelind  40059  isotone2  40448  nzin  40699  inmap  41521  islptre  41949  limccog  41950  limcresiooub  41972  limcresioolb  41973  limsupresxr  42096  liminfresxr  42097  liminfvalxr  42113  fourierdlem48  42488  fourierdlem49  42489  fourierdlem113  42553  pimiooltgt  43038  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  sssmf  43064  smflimlem2  43097  smfsuplem1  43134  setrec2fun  44844