Theorem sslin 4193

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

Syntax hints:   → wi 4   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3909  df-ss 3919

This theorem is referenced by:  ss2in  4195  inxpssres  5633  ssres2  5953  predrelss  6284  sbthlem7  9006  kmlem5  10043  canthnum  10537  ioodisj  13379  hashun3  14288  dprdres  19940  dprd2da  19954  dmdprdsplit2lem  19957  srhmsubc  20593  rhmsubclem3  20600  fldc  20697  fldhmsubc  20698  cnprest  23202  isnrm3  23272  regsep2  23289  llycmpkgen2  23463  kqdisj  23645  regr1lem  23652  fclsbas  23934  fclscf  23938  flimfnfcls  23941  isfcf  23947  metdstri  24765  nulmbl2  25462  uniioombllem4  25512  volsup2  25531  volcn  25532  itg1climres  25640  limcresi  25811  limciun  25820  rlimcnp2  26901  rplogsum  27463  chssoc  31471  cmbr4i  31576  5oai  31636  3oalem6  31642  mdslmd4i  32308  atcvat4i  32372  imadifxp  32576  swrdrndisj  32933  1arithufdlem4  33507  crefss  33857  pnfneige0  33959  cldbnd  36359  neibastop1  36392  neibastop2  36394  onint1  36482  oninhaus  36483  bj-idres  37193  cntotbnd  37835  polcon3N  39955  osumcllem4N  39997  lcfrlem2  41581  mapfzcons1  42749  coeq0i  42785  eldioph4b  42843  icccncfext  45924  rhmsubcALTVlem4  48314  srhmsubcALTV  48355  fldcALTV  48362  fldhmsubcALTV  48363  ssdisjdr  48839  sepnsepolem2  48953