Theorem sslin 4196

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 4195	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4163	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4163	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 3991	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  ss2in  4198  inxpssres  5680  ssres2  6005  predrelss  6340  sbthlem7  9082  kmlem5  10139  canthnum  10635  ioodisj  13510  hashun3  14422  dprdres  20101  dprd2da  20115  dmdprdsplit2lem  20118  srhmsubc  20766  rhmsubclem3  20773  fldc  20868  fldhmsubc  20869  cnprest  23427  isnrm3  23497  regsep2  23514  llycmpkgen2  23688  kqdisj  23870  regr1lem  23877  fclsbas  24159  fclscf  24163  flimfnfcls  24166  isfcf  24172  metdstri  24990  nulmbl2  25676  uniioombllem4  25726  volsup2  25745  volcn  25746  itg1climres  25854  limcresi  26025  limciun  26034  rlimcnp2  27112  rplogsum  27672  chssoc  31829  cmbr4i  31934  5oai  31994  3oalem6  32000  mdslmd4i  32666  atcvat4i  32730  imadifxp  32927  swrdrndisj  33258  1arithufdlem4  33818  crefss  34220  pnfneige0  34322  cldbnd  36818  neibastop1  36851  neibastop2  36853  onint1  36941  oninhaus  36942  bj-idres  37785  cntotbnd  38428  polcon3N  40672  osumcllem4N  40714  lcfrlem2  42298  mapfzcons1  43431  coeq0i  43467  eldioph4b  43521  icccncfext  46584  rhmsubcALTVlem4  49032  srhmsubcALTV  49073  fldcALTV  49080  fldhmsubcALTV  49081  ssdisjdr  49570  sepnsepolem2  49684