Theorem sslin 4178

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 4177	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4145	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4145	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 3975	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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  ss2in  4180  inxpssres  5642  ssres2  5963  predrelss  6295  sbthlem7  9028  kmlem5  10075  canthnum  10570  ioodisj  13433  hashun3  14344  dprdres  20003  dprd2da  20017  dmdprdsplit2lem  20020  srhmsubc  20659  rhmsubclem3  20666  fldc  20763  fldhmsubc  20764  cnprest  23279  isnrm3  23349  regsep2  23366  llycmpkgen2  23540  kqdisj  23722  regr1lem  23729  fclsbas  24011  fclscf  24015  flimfnfcls  24018  isfcf  24024  metdstri  24842  nulmbl2  25528  uniioombllem4  25578  volsup2  25597  volcn  25598  itg1climres  25706  limcresi  25877  limciun  25886  rlimcnp2  26955  rplogsum  27515  chssoc  31592  cmbr4i  31697  5oai  31757  3oalem6  31763  mdslmd4i  32429  atcvat4i  32493  imadifxp  32697  swrdrndisj  33043  1arithufdlem4  33637  crefss  34040  pnfneige0  34142  cldbnd  36561  neibastop1  36594  neibastop2  36596  onint1  36684  oninhaus  36685  bj-idres  37527  cntotbnd  38170  polcon3N  40416  osumcllem4N  40458  lcfrlem2  42042  mapfzcons1  43173  coeq0i  43209  eldioph4b  43263  icccncfext  46337  rhmsubcALTVlem4  48782  srhmsubcALTV  48823  fldcALTV  48830  fldhmsubcALTV  48831  ssdisjdr  49306  sepnsepolem2  49420