Theorem sslin 4183

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

Syntax hints:   → wi 4   ∩ cin 3888   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  ss2in  4185  inxpssres  5648  ssres2  5969  predrelss  6301  sbthlem7  9031  kmlem5  10077  canthnum  10572  ioodisj  13435  hashun3  14346  dprdres  20005  dprd2da  20019  dmdprdsplit2lem  20022  srhmsubc  20657  rhmsubclem3  20664  fldc  20761  fldhmsubc  20762  cnprest  23254  isnrm3  23324  regsep2  23341  llycmpkgen2  23515  kqdisj  23697  regr1lem  23704  fclsbas  23986  fclscf  23990  flimfnfcls  23993  isfcf  23999  metdstri  24817  nulmbl2  25503  uniioombllem4  25553  volsup2  25572  volcn  25573  itg1climres  25681  limcresi  25852  limciun  25861  rlimcnp2  26930  rplogsum  27490  chssoc  31567  cmbr4i  31672  5oai  31732  3oalem6  31738  mdslmd4i  32404  atcvat4i  32468  imadifxp  32671  swrdrndisj  33017  1arithufdlem4  33607  crefss  33993  pnfneige0  34095  cldbnd  36508  neibastop1  36541  neibastop2  36543  onint1  36631  oninhaus  36632  bj-idres  37474  cntotbnd  38117  polcon3N  40363  osumcllem4N  40405  lcfrlem2  41989  mapfzcons1  43149  coeq0i  43185  eldioph4b  43239  icccncfext  46315  rhmsubcALTVlem4  48760  srhmsubcALTV  48801  fldcALTV  48808  fldhmsubcALTV  48809  ssdisjdr  49284  sepnsepolem2  49398