Theorem sslin 4065

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

Syntax hints:   → wi 4   ∩ cin 3797   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812

This theorem is referenced by:  ss2in  4067  inxpssres  5363  ssres2  5665  sbthlem7  8351  kmlem5  9298  canthnum  9793  ioodisj  12602  hashun3  13470  xpsc0  16580  dprdres  18788  dprd2da  18802  dmdprdsplit2lem  18805  cnprest  21471  isnrm3  21541  regsep2  21558  llycmpkgen2  21731  kqdisj  21913  regr1lem  21920  fclsbas  22202  fclscf  22206  flimfnfcls  22209  isfcf  22215  metdstri  23031  nulmbl2  23709  uniioombllem4  23759  volsup2  23778  volcn  23779  itg1climres  23887  limcresi  24055  limciun  24064  rlimcnp2  25113  rplogsum  25636  chssoc  28906  cmbr4i  29011  5oai  29071  3oalem6  29077  mdslmd4i  29743  atcvat4i  29807  imadifxp  29957  crefss  30457  pnfneige0  30538  cldbnd  32854  neibastop1  32887  neibastop2  32889  onint1  32976  oninhaus  32977  cntotbnd  34132  polcon3N  35987  osumcllem4N  36029  lcfrlem2  37613  mapfzcons1  38119  coeq0i  38155  eldioph4b  38214  icccncfext  40889  srhmsubc  42937  fldc  42944  fldhmsubc  42945  rhmsubclem3  42949  srhmsubcALTV  42955  fldcALTV  42962  fldhmsubcALTV  42963  rhmsubcALTVlem4  42968