Theorem sslin 4194

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3911  df-ss 3921

This theorem is referenced by:  ss2in  4196  inxpssres  5662  ssres2  5988  predrelss  6320  sbthlem7  9061  kmlem5  10108  canthnum  10604  ioodisj  13483  hashun3  14394  dprdres  20053  dprd2da  20067  dmdprdsplit2lem  20070  srhmsubc  20709  rhmsubclem3  20716  fldc  20813  fldhmsubc  20814  cnprest  23329  isnrm3  23399  regsep2  23416  llycmpkgen2  23590  kqdisj  23772  regr1lem  23779  fclsbas  24061  fclscf  24065  flimfnfcls  24068  isfcf  24074  metdstri  24892  nulmbl2  25578  uniioombllem4  25628  volsup2  25647  volcn  25648  itg1climres  25756  limcresi  25927  limciun  25936  rlimcnp2  27008  rplogsum  27568  chssoc  31645  cmbr4i  31750  5oai  31810  3oalem6  31816  mdslmd4i  32482  atcvat4i  32546  imadifxp  32750  swrdrndisj  33096  1arithufdlem4  33704  crefss  34107  pnfneige0  34209  cldbnd  36650  neibastop1  36683  neibastop2  36685  onint1  36773  oninhaus  36774  bj-idres  37616  cntotbnd  38259  polcon3N  40505  osumcllem4N  40547  lcfrlem2  42131  mapfzcons1  43262  coeq0i  43298  eldioph4b  43352  icccncfext  46425  rhmsubcALTVlem4  48870  srhmsubcALTV  48911  fldcALTV  48918  fldhmsubcALTV  48919  ssdisjdr  49394  sepnsepolem2  49508