Theorem sslin 4218

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

Syntax hints:   → wi 4   ∩ cin 3925   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  ss2in  4220  inxpssres  5671  ssres2  5991  predrelss  6326  sbthlem7  9103  kmlem5  10169  canthnum  10663  ioodisj  13499  hashun3  14402  dprdres  20011  dprd2da  20025  dmdprdsplit2lem  20028  srhmsubc  20640  rhmsubclem3  20647  fldc  20744  fldhmsubc  20745  cnprest  23227  isnrm3  23297  regsep2  23314  llycmpkgen2  23488  kqdisj  23670  regr1lem  23677  fclsbas  23959  fclscf  23963  flimfnfcls  23966  isfcf  23972  metdstri  24791  nulmbl2  25489  uniioombllem4  25539  volsup2  25558  volcn  25559  itg1climres  25667  limcresi  25838  limciun  25847  rlimcnp2  26928  rplogsum  27490  chssoc  31477  cmbr4i  31582  5oai  31642  3oalem6  31648  mdslmd4i  32314  atcvat4i  32378  imadifxp  32582  swrdrndisj  32933  1arithufdlem4  33562  crefss  33880  pnfneige0  33982  cldbnd  36344  neibastop1  36377  neibastop2  36379  onint1  36467  oninhaus  36468  bj-idres  37178  cntotbnd  37820  polcon3N  39936  osumcllem4N  39978  lcfrlem2  41562  mapfzcons1  42740  coeq0i  42776  eldioph4b  42834  icccncfext  45916  rhmsubcALTVlem4  48259  srhmsubcALTV  48300  fldcALTV  48307  fldhmsubcALTV  48308  ssdisjdr  48787  sepnsepolem2  48897