Theorem sslin 4192

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

Syntax hints:   → wi 4   ∩ cin 3897   ⊆ wss 3898

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  ss2in  4194  inxpssres  5636  ssres2  5957  predrelss  6289  sbthlem7  9013  kmlem5  10053  canthnum  10547  ioodisj  13384  hashun3  14293  dprdres  19944  dprd2da  19958  dmdprdsplit2lem  19961  srhmsubc  20597  rhmsubclem3  20604  fldc  20701  fldhmsubc  20702  cnprest  23205  isnrm3  23275  regsep2  23292  llycmpkgen2  23466  kqdisj  23648  regr1lem  23655  fclsbas  23937  fclscf  23941  flimfnfcls  23944  isfcf  23950  metdstri  24768  nulmbl2  25465  uniioombllem4  25515  volsup2  25534  volcn  25535  itg1climres  25643  limcresi  25814  limciun  25823  rlimcnp2  26904  rplogsum  27466  chssoc  31478  cmbr4i  31583  5oai  31643  3oalem6  31649  mdslmd4i  32315  atcvat4i  32379  imadifxp  32583  swrdrndisj  32945  1arithufdlem4  33519  crefss  33883  pnfneige0  33985  cldbnd  36391  neibastop1  36424  neibastop2  36426  onint1  36514  oninhaus  36515  bj-idres  37225  cntotbnd  37856  polcon3N  40036  osumcllem4N  40078  lcfrlem2  41662  mapfzcons1  42834  coeq0i  42870  eldioph4b  42928  icccncfext  46009  rhmsubcALTVlem4  48408  srhmsubcALTV  48449  fldcALTV  48456  fldhmsubcALTV  48457  ssdisjdr  48933  sepnsepolem2  49047