Theorem sslin 4184

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

Syntax hints:   → wi 4   ∩ cin 3889   ⊆ wss 3890

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 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  ss2in  4186  inxpssres  5641  ssres2  5963  predrelss  6295  sbthlem7  9024  kmlem5  10068  canthnum  10563  ioodisj  13426  hashun3  14337  dprdres  19996  dprd2da  20010  dmdprdsplit2lem  20013  srhmsubc  20648  rhmsubclem3  20655  fldc  20752  fldhmsubc  20753  cnprest  23264  isnrm3  23334  regsep2  23351  llycmpkgen2  23525  kqdisj  23707  regr1lem  23714  fclsbas  23996  fclscf  24000  flimfnfcls  24003  isfcf  24009  metdstri  24827  nulmbl2  25513  uniioombllem4  25563  volsup2  25582  volcn  25583  itg1climres  25691  limcresi  25862  limciun  25871  rlimcnp2  26943  rplogsum  27504  chssoc  31582  cmbr4i  31687  5oai  31747  3oalem6  31753  mdslmd4i  32419  atcvat4i  32483  imadifxp  32686  swrdrndisj  33032  1arithufdlem4  33622  crefss  34009  pnfneige0  34111  cldbnd  36524  neibastop1  36557  neibastop2  36559  onint1  36647  oninhaus  36648  bj-idres  37490  cntotbnd  38131  polcon3N  40377  osumcllem4N  40419  lcfrlem2  42003  mapfzcons1  43163  coeq0i  43199  eldioph4b  43257  icccncfext  46333  rhmsubcALTVlem4  48772  srhmsubcALTV  48813  fldcALTV  48820  fldhmsubcALTV  48821  ssdisjdr  49296  sepnsepolem2  49410