Theorem sslin 4195

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

Syntax hints:   → wi 4   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  ss2in  4197  inxpssres  5641  ssres2  5963  predrelss  6295  sbthlem7  9021  kmlem5  10065  canthnum  10560  ioodisj  13398  hashun3  14307  dprdres  19959  dprd2da  19973  dmdprdsplit2lem  19976  srhmsubc  20613  rhmsubclem3  20620  fldc  20717  fldhmsubc  20718  cnprest  23233  isnrm3  23303  regsep2  23320  llycmpkgen2  23494  kqdisj  23676  regr1lem  23683  fclsbas  23965  fclscf  23969  flimfnfcls  23972  isfcf  23978  metdstri  24796  nulmbl2  25493  uniioombllem4  25543  volsup2  25562  volcn  25563  itg1climres  25671  limcresi  25842  limciun  25851  rlimcnp2  26932  rplogsum  27494  chssoc  31571  cmbr4i  31676  5oai  31736  3oalem6  31742  mdslmd4i  32408  atcvat4i  32472  imadifxp  32676  swrdrndisj  33039  1arithufdlem4  33628  crefss  34006  pnfneige0  34108  cldbnd  36520  neibastop1  36553  neibastop2  36555  onint1  36643  oninhaus  36644  bj-idres  37361  cntotbnd  37993  polcon3N  40173  osumcllem4N  40215  lcfrlem2  41799  mapfzcons1  42955  coeq0i  42991  eldioph4b  43049  icccncfext  46127  rhmsubcALTVlem4  48526  srhmsubcALTV  48567  fldcALTV  48574  fldhmsubcALTV  48575  ssdisjdr  49050  sepnsepolem2  49164