Theorem sslin 4125

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

Syntax hints:   → wi 4   ∩ cin 3842   ⊆ wss 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-rab 3062  df-v 3400  df-in 3850  df-ss 3860

This theorem is referenced by:  ss2in  4127  inxpssres  5542  ssres2  5853  sbthlem7  8685  kmlem5  9656  canthnum  10151  ioodisj  12958  hashun3  13839  dprdres  19271  dprd2da  19285  dmdprdsplit2lem  19288  cnprest  22042  isnrm3  22112  regsep2  22129  llycmpkgen2  22303  kqdisj  22485  regr1lem  22492  fclsbas  22774  fclscf  22778  flimfnfcls  22781  isfcf  22787  metdstri  23605  nulmbl2  24290  uniioombllem4  24340  volsup2  24359  volcn  24360  itg1climres  24469  limcresi  24639  limciun  24648  rlimcnp2  25706  rplogsum  26265  chssoc  29433  cmbr4i  29538  5oai  29598  3oalem6  29604  mdslmd4i  30270  atcvat4i  30334  imadifxp  30516  swrdrndisj  30806  crefss  31373  pnfneige0  31475  cldbnd  34160  neibastop1  34193  neibastop2  34195  onint1  34283  oninhaus  34284  bj-idres  34974  cntotbnd  35599  polcon3N  37576  osumcllem4N  37618  lcfrlem2  39202  mapfzcons1  40133  coeq0i  40169  eldioph4b  40227  icccncfext  42992  srhmsubc  45197  fldc  45204  fldhmsubc  45205  rhmsubclem3  45209  srhmsubcALTV  45215  fldcALTV  45222  fldhmsubcALTV  45223  rhmsubcALTVlem4  45228  ssdisjdr  45715  sepnsepolem2  45767