Theorem sslin 4188

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

This proof depends on syntax axioms:   → wi 4   ∩ cin 3898   ⊆ wss 3899

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  ss2in  4190  inxpssres  5668  ssres2  5995  predrelss  6333  sbthlem7  9096  kmlem5  10214  canthnum  10715  ioodisj  13594  hashun3  14508  dprdres  20224  dprd2da  20238  dmdprdsplit2lem  20241  srhmsubc  20912  rhmsubclem3  20919  fldc  21021  fldhmsubc  21022  cnprest  23587  isnrm3  23657  regsep2  23674  llycmpkgen2  23849  kqdisj  24031  regr1lem  24038  fclsbas  24320  fclscf  24324  flimfnfcls  24327  isfcf  24333  metdstri  25151  nulmbl2  25837  uniioombllem4  25887  volsup2  25906  volcn  25907  itg1climres  26015  limcresi  26185  limciun  26194  rlimcnp2  27276  rplogsum  27836  chssoc  32080  cmbr4i  32185  5oai  32245  3oalem6  32251  mdslmd4i  32917  atcvat4i  32981  imadifxp  33177  swrdrndisj  33500  1arithufdlem4  34061  crefss  34463  pnfneige0  34565  cldbnd  37084  neibastop1  37117  neibastop2  37119  onint1  37207  oninhaus  37208  bj-idres  38049  cntotbnd  38698  polcon3N  40942  osumcllem4N  40984  lcfrlem2  42568  mapfzcons1  43681  coeq0i  43717  eldioph4b  43771  icccncfext  46841  rhmsubcALTVlem4  49325  srhmsubcALTV  49366  fldcALTV  49373  fldhmsubcALTV  49374  ssdisjdr  49863  sepnsepolem2  49975