Theorem sslin 4197

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

Syntax hints:   → wi 4   ∩ cin 3902   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  ss2in  4199  inxpssres  5649  ssres2  5971  predrelss  6303  sbthlem7  9033  kmlem5  10077  canthnum  10572  ioodisj  13410  hashun3  14319  dprdres  19971  dprd2da  19985  dmdprdsplit2lem  19988  srhmsubc  20625  rhmsubclem3  20632  fldc  20729  fldhmsubc  20730  cnprest  23245  isnrm3  23315  regsep2  23332  llycmpkgen2  23506  kqdisj  23688  regr1lem  23695  fclsbas  23977  fclscf  23981  flimfnfcls  23984  isfcf  23990  metdstri  24808  nulmbl2  25505  uniioombllem4  25555  volsup2  25574  volcn  25575  itg1climres  25683  limcresi  25854  limciun  25863  rlimcnp2  26944  rplogsum  27506  chssoc  31583  cmbr4i  31688  5oai  31748  3oalem6  31754  mdslmd4i  32420  atcvat4i  32484  imadifxp  32687  swrdrndisj  33049  1arithufdlem4  33639  crefss  34026  pnfneige0  34128  cldbnd  36539  neibastop1  36572  neibastop2  36574  onint1  36662  oninhaus  36663  bj-idres  37409  cntotbnd  38041  polcon3N  40287  osumcllem4N  40329  lcfrlem2  41913  mapfzcons1  43068  coeq0i  43104  eldioph4b  43162  icccncfext  46239  rhmsubcALTVlem4  48638  srhmsubcALTV  48679  fldcALTV  48686  fldhmsubcALTV  48687  ssdisjdr  49162  sepnsepolem2  49276