Theorem ltadd2dd 9820

Description: Addition to both sides of 'less than'. (Contributed by Mario Carneiro, 30-May-2016.)

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltd.2	|- ( ph -> B e. RR )
letrd.3	|- ( ph -> C e. RR )
ltletrd.4	|- ( ph -> A < B )

Assertion

Ref	Expression
ltadd2dd	|- ( ph -> ( C + A ) < ( C + B ) )

Proof of Theorem ltadd2dd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 |- ( ph -> A < B )
2		ltd.1	. . 3 |- ( ph -> A e. RR )
3		ltd.2	. . 3 |- ( ph -> B e. RR )
4		letrd.3	. . 3 |- ( ph -> C e. RR )
5	2, 3, 4	ltadd2d 9817	. 2 |- ( ph -> ( A < B <-> ( C + A ) < ( C + B ) ) )
6	1, 5	mpbid 215	1 |- ( ph -> ( C + A ) < ( C + B ) )

Syntax hints:   -> wi 4   e. wcel 1898   class class class wbr 4416  (class class class)co 6315   RRcr 9564   + caddc 9568   < clt 9701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-addrcl 9626  ax-pre-lttri 9639  ax-pre-ltadd 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706

This theorem is referenced by:  ccatrn  12769  eirrlem  14305  prmreclem5  14913  iccntr  21888  icccmplem2  21890  ivthlem2  22452  uniioombllem3  22592  opnmbllem  22608  dvcnvre  23020  cosordlem  23529  efif1olem2  23541  atanlogaddlem  23888  pntibndlem2  24478  pntlemr  24489  dya2icoseg  29148  opnmbllem0  32021  binomcxplemdvbinom  36746  zltlesub  37533  supxrge  37599  ltadd12dd  37604  0ellimcdiv  37768  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  stoweidlem11  37909  stoweidlem14  37912  stoweidlem26  37924  stoweidlem44  37943  dirkertrigeqlem3  38000  dirkercncflem1  38003  dirkercncflem2  38004  fourierdlem4  38011  fourierdlem10  38017  fourierdlem28  38035  fourierdlem40  38048  fourierdlem50  38058  fourierdlem57  38065  fourierdlem59  38067  fourierdlem60  38068  fourierdlem61  38069  fourierdlem68  38076  fourierdlem74  38082  fourierdlem75  38083  fourierdlem76  38084  fourierdlem78  38086  fourierdlem79  38087  fourierdlem84  38092  fourierdlem93  38101  fourierdlem111  38119  fouriersw  38133