Theorem sslin 4191

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3901   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  ss2in  4193  inxpssres  5676  ssres2  6001  predrelss  6339  sbthlem7  9095  kmlem5  10161  canthnum  10662  ioodisj  13539  hashun3  14452  dprdres  20163  dprd2da  20177  dmdprdsplit2lem  20180  srhmsubc  20848  rhmsubclem3  20855  fldc  20956  fldhmsubc  20957  cnprest  23520  isnrm3  23590  regsep2  23607  llycmpkgen2  23782  kqdisj  23964  regr1lem  23971  fclsbas  24253  fclscf  24257  flimfnfcls  24260  isfcf  24266  metdstri  25084  nulmbl2  25770  uniioombllem4  25820  volsup2  25839  volcn  25840  itg1climres  25948  limcresi  26119  limciun  26128  rlimcnp2  27211  rplogsum  27771  chssoc  31985  cmbr4i  32090  5oai  32150  3oalem6  32156  mdslmd4i  32822  atcvat4i  32886  imadifxp  33082  swrdrndisj  33405  1arithufdlem4  33965  crefss  34367  pnfneige0  34469  cldbnd  36953  neibastop1  36986  neibastop2  36988  onint1  37076  oninhaus  37077  bj-idres  37920  cntotbnd  38554  polcon3N  40798  osumcllem4N  40840  lcfrlem2  42424  mapfzcons1  43570  coeq0i  43606  eldioph4b  43660  icccncfext  46723  rhmsubcALTVlem4  49207  srhmsubcALTV  49248  fldcALTV  49255  fldhmsubcALTV  49256  ssdisjdr  49745  sepnsepolem2  49857