Theorem sslin 4161

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)

Assertion

Ref	Expression
sslin	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Proof of Theorem sslin

Step	Hyp	Ref	Expression
1		ssrin 4160	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4128	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4128	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 3960	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  ss2in  4163  inxpssres  5536  ssres2  5846  sbthlem7  8617  kmlem5  9565  canthnum  10060  ioodisj  12860  hashun3  13741  dprdres  19143  dprd2da  19157  dmdprdsplit2lem  19160  cnprest  21894  isnrm3  21964  regsep2  21981  llycmpkgen2  22155  kqdisj  22337  regr1lem  22344  fclsbas  22626  fclscf  22630  flimfnfcls  22633  isfcf  22639  metdstri  23456  nulmbl2  24140  uniioombllem4  24190  volsup2  24209  volcn  24210  itg1climres  24318  limcresi  24488  limciun  24497  rlimcnp2  25552  rplogsum  26111  chssoc  29279  cmbr4i  29384  5oai  29444  3oalem6  29450  mdslmd4i  30116  atcvat4i  30180  imadifxp  30364  swrdrndisj  30657  crefss  31202  pnfneige0  31304  cldbnd  33787  neibastop1  33820  neibastop2  33822  onint1  33910  oninhaus  33911  bj-idres  34575  cntotbnd  35234  polcon3N  37213  osumcllem4N  37255  lcfrlem2  38839  mapfzcons1  39658  coeq0i  39694  eldioph4b  39752  icccncfext  42529  srhmsubc  44700  fldc  44707  fldhmsubc  44708  rhmsubclem3  44712  srhmsubcALTV  44718  fldcALTV  44725  fldhmsubcALTV  44726  rhmsubcALTVlem4  44731