Theorem sslin 4206

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

Syntax hints:   → wi 4   ∩ cin 3913   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  ss2in  4208  inxpssres  5655  ssres2  5975  predrelss  6310  sbthlem7  9057  kmlem5  10108  canthnum  10602  ioodisj  13443  hashun3  14349  dprdres  19960  dprd2da  19974  dmdprdsplit2lem  19977  srhmsubc  20589  rhmsubclem3  20596  fldc  20693  fldhmsubc  20694  cnprest  23176  isnrm3  23246  regsep2  23263  llycmpkgen2  23437  kqdisj  23619  regr1lem  23626  fclsbas  23908  fclscf  23912  flimfnfcls  23915  isfcf  23921  metdstri  24740  nulmbl2  25437  uniioombllem4  25487  volsup2  25506  volcn  25507  itg1climres  25615  limcresi  25786  limciun  25795  rlimcnp2  26876  rplogsum  27438  chssoc  31425  cmbr4i  31530  5oai  31590  3oalem6  31596  mdslmd4i  32262  atcvat4i  32326  imadifxp  32530  swrdrndisj  32879  1arithufdlem4  33518  crefss  33839  pnfneige0  33941  cldbnd  36314  neibastop1  36347  neibastop2  36349  onint1  36437  oninhaus  36438  bj-idres  37148  cntotbnd  37790  polcon3N  39911  osumcllem4N  39953  lcfrlem2  41537  mapfzcons1  42705  coeq0i  42741  eldioph4b  42799  icccncfext  45885  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  fldcALTV  48320  fldhmsubcALTV  48321  ssdisjdr  48797  sepnsepolem2  48911