Theorem sslin 4234

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

Syntax hints:   → wi 4   ∩ cin 3947   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  ss2in  4236  inxpssres  5693  ssres2  6009  predrelss  6338  sbthlem7  9091  kmlem5  10151  canthnum  10646  ioodisj  13463  hashun3  14348  dprdres  19939  dprd2da  19953  dmdprdsplit2lem  19956  cnprest  23013  isnrm3  23083  regsep2  23100  llycmpkgen2  23274  kqdisj  23456  regr1lem  23463  fclsbas  23745  fclscf  23749  flimfnfcls  23752  isfcf  23758  metdstri  24587  nulmbl2  25277  uniioombllem4  25327  volsup2  25346  volcn  25347  itg1climres  25456  limcresi  25626  limciun  25635  rlimcnp2  26695  rplogsum  27254  chssoc  31004  cmbr4i  31109  5oai  31169  3oalem6  31175  mdslmd4i  31841  atcvat4i  31905  imadifxp  32087  swrdrndisj  32376  crefss  33115  pnfneige0  33217  cldbnd  35514  neibastop1  35547  neibastop2  35549  onint1  35637  oninhaus  35638  bj-idres  36344  cntotbnd  36967  polcon3N  39091  osumcllem4N  39133  lcfrlem2  40717  mapfzcons1  41757  coeq0i  41793  eldioph4b  41851  icccncfext  44902  srhmsubc  47063  fldc  47070  fldhmsubc  47071  rhmsubclem3  47075  srhmsubcALTV  47081  fldcALTV  47088  fldhmsubcALTV  47089  rhmsubcALTVlem4  47094  ssdisjdr  47581  sepnsepolem2  47643