Theorem sslin 4233

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

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

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 3954  df-ss 3964

This theorem is referenced by:  ss2in  4235  inxpssres  5692  ssres2  6007  predrelss  6335  sbthlem7  9085  kmlem5  10145  canthnum  10640  ioodisj  13455  hashun3  14340  dprdres  19892  dprd2da  19906  dmdprdsplit2lem  19909  cnprest  22784  isnrm3  22854  regsep2  22871  llycmpkgen2  23045  kqdisj  23227  regr1lem  23234  fclsbas  23516  fclscf  23520  flimfnfcls  23523  isfcf  23529  metdstri  24358  nulmbl2  25044  uniioombllem4  25094  volsup2  25113  volcn  25114  itg1climres  25223  limcresi  25393  limciun  25402  rlimcnp2  26460  rplogsum  27019  chssoc  30736  cmbr4i  30841  5oai  30901  3oalem6  30907  mdslmd4i  31573  atcvat4i  31637  imadifxp  31819  swrdrndisj  32108  crefss  32817  pnfneige0  32919  cldbnd  35199  neibastop1  35232  neibastop2  35234  onint1  35322  oninhaus  35323  bj-idres  36029  cntotbnd  36652  polcon3N  38776  osumcllem4N  38818  lcfrlem2  40402  mapfzcons1  41440  coeq0i  41476  eldioph4b  41534  icccncfext  44589  srhmsubc  46927  fldc  46934  fldhmsubc  46935  rhmsubclem3  46939  srhmsubcALTV  46945  fldcALTV  46952  fldhmsubcALTV  46953  rhmsubcALTVlem4  46958  ssdisjdr  47446  sepnsepolem2  47508