Theorem sslin 3801

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

Syntax hints:   → wi 4   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  ss2in  3802  ssres2  5345  ssrnres  5491  sbthlem7  7961  kmlem5  8859  canthnum  9350  ioodisj  12173  hashun3  13034  xpsc0  16043  dprdres  18250  dprd2da  18264  dmdprdsplit2lem  18267  cnprest  20903  isnrm3  20973  regsep2  20990  llycmpkgen2  21163  kqdisj  21345  regr1lem  21352  fclsbas  21635  fclscf  21639  flimfnfcls  21642  isfcf  21648  metdstri  22462  nulmbl2  23111  uniioombllem4  23160  volsup2  23179  volcn  23180  itg1climres  23287  limcresi  23455  limciun  23464  rlimcnp2  24493  rplogsum  25016  chssoc  27739  cmbr4i  27844  5oai  27904  3oalem6  27910  mdslmd4i  28576  atcvat4i  28640  imadifxp  28796  crefss  29244  pnfneige0  29325  cldbnd  31491  neibastop1  31524  neibastop2  31526  onint1  31618  oninhaus  31619  cntotbnd  32765  polcon3N  34221  osumcllem4N  34263  lcfrlem2  35850  mapfzcons1  36298  coeq0i  36334  eldioph4b  36393  icccncfext  38773  srhmsubc  41868  fldc  41875  fldhmsubc  41876  rhmsubclem3  41880  srhmsubcALTV  41887  fldcALTV  41894  fldhmsubcALTV  41895  rhmsubcALTVlem4  41900