Theorem sslin 4197

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

Syntax hints:   → wi 4   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  ss2in  4199  inxpssres  5669  ssres2  5994  predrelss  6328  sbthlem7  9069  kmlem5  10126  canthnum  10622  ioodisj  13500  hashun3  14411  dprdres  20091  dprd2da  20105  dmdprdsplit2lem  20108  srhmsubc  20756  rhmsubclem3  20763  fldc  20856  fldhmsubc  20857  cnprest  23407  isnrm3  23477  regsep2  23494  llycmpkgen2  23668  kqdisj  23850  regr1lem  23857  fclsbas  24139  fclscf  24143  flimfnfcls  24146  isfcf  24152  metdstri  24970  nulmbl2  25656  uniioombllem4  25706  volsup2  25725  volcn  25726  itg1climres  25834  limcresi  26005  limciun  26014  rlimcnp2  27089  rplogsum  27649  chssoc  31757  cmbr4i  31862  5oai  31922  3oalem6  31928  mdslmd4i  32594  atcvat4i  32658  imadifxp  32856  swrdrndisj  33190  1arithufdlem4  33754  crefss  34156  pnfneige0  34258  cldbnd  36699  neibastop1  36732  neibastop2  36734  onint1  36822  oninhaus  36823  bj-idres  37664  cntotbnd  38307  polcon3N  40553  osumcllem4N  40595  lcfrlem2  42179  mapfzcons1  43310  coeq0i  43346  eldioph4b  43400  icccncfext  46459  rhmsubcALTVlem4  48904  srhmsubcALTV  48945  fldcALTV  48952  fldhmsubcALTV  48953  ssdisjdr  49438  sepnsepolem2  49552