Theorem sslin 4196

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

Syntax hints:   → wi 4   ∩ cin 3904   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  ss2in  4198  inxpssres  5640  ssres2  5959  predrelss  6289  sbthlem7  9017  kmlem5  10068  canthnum  10562  ioodisj  13403  hashun3  14309  dprdres  19927  dprd2da  19941  dmdprdsplit2lem  19944  srhmsubc  20583  rhmsubclem3  20590  fldc  20687  fldhmsubc  20688  cnprest  23192  isnrm3  23262  regsep2  23279  llycmpkgen2  23453  kqdisj  23635  regr1lem  23642  fclsbas  23924  fclscf  23928  flimfnfcls  23931  isfcf  23937  metdstri  24756  nulmbl2  25453  uniioombllem4  25503  volsup2  25522  volcn  25523  itg1climres  25631  limcresi  25802  limciun  25811  rlimcnp2  26892  rplogsum  27454  chssoc  31458  cmbr4i  31563  5oai  31623  3oalem6  31629  mdslmd4i  32295  atcvat4i  32359  imadifxp  32563  swrdrndisj  32912  1arithufdlem4  33494  crefss  33815  pnfneige0  33917  cldbnd  36299  neibastop1  36332  neibastop2  36334  onint1  36422  oninhaus  36423  bj-idres  37133  cntotbnd  37775  polcon3N  39896  osumcllem4N  39938  lcfrlem2  41522  mapfzcons1  42690  coeq0i  42726  eldioph4b  42784  icccncfext  45869  rhmsubcALTVlem4  48269  srhmsubcALTV  48310  fldcALTV  48317  fldhmsubcALTV  48318  ssdisjdr  48794  sepnsepolem2  48908