Theorem sslin 4168

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

Syntax hints:   → wi 4   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  ss2in  4170  inxpssres  5606  ssres2  5919  predrelss  6240  sbthlem7  8876  kmlem5  9910  canthnum  10405  ioodisj  13214  hashun3  14099  dprdres  19631  dprd2da  19645  dmdprdsplit2lem  19648  cnprest  22440  isnrm3  22510  regsep2  22527  llycmpkgen2  22701  kqdisj  22883  regr1lem  22890  fclsbas  23172  fclscf  23176  flimfnfcls  23179  isfcf  23185  metdstri  24014  nulmbl2  24700  uniioombllem4  24750  volsup2  24769  volcn  24770  itg1climres  24879  limcresi  25049  limciun  25058  rlimcnp2  26116  rplogsum  26675  chssoc  29858  cmbr4i  29963  5oai  30023  3oalem6  30029  mdslmd4i  30695  atcvat4i  30759  imadifxp  30940  swrdrndisj  31229  crefss  31799  pnfneige0  31901  cldbnd  34515  neibastop1  34548  neibastop2  34550  onint1  34638  oninhaus  34639  bj-idres  35331  cntotbnd  35954  polcon3N  37931  osumcllem4N  37973  lcfrlem2  39557  mapfzcons1  40539  coeq0i  40575  eldioph4b  40633  icccncfext  43428  srhmsubc  45634  fldc  45641  fldhmsubc  45642  rhmsubclem3  45646  srhmsubcALTV  45652  fldcALTV  45659  fldhmsubcALTV  45660  rhmsubcALTVlem4  45665  ssdisjdr  46154  sepnsepolem2  46216