Theorem sslin 4264

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

Syntax hints:   → wi 4   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  ss2in  4266  inxpssres  5717  ssres2  6034  predrelss  6369  sbthlem7  9155  kmlem5  10224  canthnum  10718  ioodisj  13542  hashun3  14433  dprdres  20072  dprd2da  20086  dmdprdsplit2lem  20089  srhmsubc  20702  rhmsubclem3  20709  fldc  20807  fldhmsubc  20808  cnprest  23318  isnrm3  23388  regsep2  23405  llycmpkgen2  23579  kqdisj  23761  regr1lem  23768  fclsbas  24050  fclscf  24054  flimfnfcls  24057  isfcf  24063  metdstri  24892  nulmbl2  25590  uniioombllem4  25640  volsup2  25659  volcn  25660  itg1climres  25769  limcresi  25940  limciun  25949  rlimcnp2  27027  rplogsum  27589  chssoc  31528  cmbr4i  31633  5oai  31693  3oalem6  31699  mdslmd4i  32365  atcvat4i  32429  imadifxp  32623  swrdrndisj  32924  1arithufdlem4  33540  crefss  33795  pnfneige0  33897  cldbnd  36292  neibastop1  36325  neibastop2  36327  onint1  36415  oninhaus  36416  bj-idres  37126  cntotbnd  37756  polcon3N  39874  osumcllem4N  39916  lcfrlem2  41500  mapfzcons1  42673  coeq0i  42709  eldioph4b  42767  icccncfext  45808  rhmsubcALTVlem4  48007  srhmsubcALTV  48048  fldcALTV  48055  fldhmsubcALTV  48056  ssdisjdr  48540  sepnsepolem2  48602