Theorem sslin 4165

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

Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  ss2in  4167  inxpssres  5597  ssres2  5908  sbthlem7  8829  kmlem5  9841  canthnum  10336  ioodisj  13143  hashun3  14027  dprdres  19546  dprd2da  19560  dmdprdsplit2lem  19563  cnprest  22348  isnrm3  22418  regsep2  22435  llycmpkgen2  22609  kqdisj  22791  regr1lem  22798  fclsbas  23080  fclscf  23084  flimfnfcls  23087  isfcf  23093  metdstri  23920  nulmbl2  24605  uniioombllem4  24655  volsup2  24674  volcn  24675  itg1climres  24784  limcresi  24954  limciun  24963  rlimcnp2  26021  rplogsum  26580  chssoc  29759  cmbr4i  29864  5oai  29924  3oalem6  29930  mdslmd4i  30596  atcvat4i  30660  imadifxp  30841  swrdrndisj  31131  crefss  31701  pnfneige0  31803  cldbnd  34442  neibastop1  34475  neibastop2  34477  onint1  34565  oninhaus  34566  bj-idres  35258  cntotbnd  35881  polcon3N  37858  osumcllem4N  37900  lcfrlem2  39484  mapfzcons1  40455  coeq0i  40491  eldioph4b  40549  icccncfext  43318  srhmsubc  45522  fldc  45529  fldhmsubc  45530  rhmsubclem3  45534  srhmsubcALTV  45540  fldcALTV  45547  fldhmsubcALTV  45548  rhmsubcALTVlem4  45553  ssdisjdr  46042  sepnsepolem2  46104