Theorem leadd2dd 11307

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

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ltadd1d.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
leadd1dd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Assertion

Ref	Expression
leadd2dd	⊢ (𝜑 → (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))

Proof of Theorem leadd2dd

Step	Hyp	Ref	Expression
1		leadd1dd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		leidd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltnegd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ltadd1d.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5	2, 3, 4	leadd2d 11287	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 + 𝐴) ≤ (𝐶 + 𝐵)))
6	1, 5	mpbid 235	1 ⊢ (𝜑 → (𝐶 + 𝐴) ≤ (𝐶 + 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2112   class class class wbr 5037  (class class class)co 7157  ℝcr 10588   + caddc 10592   ≤ cle 10728

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-po 5448  df-so 5449  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733

This theorem is referenced by:  difgtsumgt  12001  expmulnbnd  13660  discr1  13664  hashun2  13808  abstri  14752  iseraltlem2  15101  prmreclem4  16325  tcphcphlem1  23950  trirn  24115  nulmbl2  24251  voliunlem1  24265  uniioombllem4  24301  itg2split  24464  ulmcn  25108  abslogle  25323  emcllem2  25696  lgambdd  25736  chtublem  25909  chtub  25910  logfaclbnd  25920  bcmax  25976  chebbnd1lem2  26168  rplogsumlem1  26182  selberglem2  26244  selbergb  26247  chpdifbndlem1  26251  pntpbnd1a  26283  pntpbnd2  26285  pntibndlem2  26289  pntibndlem3  26290  pntlemg  26296  pntlemr  26300  pntlemk  26304  pntlemo  26305  ostth2lem3  26333  smcnlem  28594  minvecolem3  28773  staddi  30143  stadd3i  30145  nexple  31510  fsum2dsub  32120  resconn  32738  itg2addnc  35427  ftc1anclem8  35453  lcmineqlem22  39653  aks4d1p1p2  39672  aks4d1p1p5  39677  pell1qrgaplem  40233  leadd12dd  42362  ioodvbdlimc1lem2  42986  stoweidlem11  43065  stoweidlem26  43080  stirlinglem8  43135  stirlinglem12  43139  fourierdlem4  43165  fourierdlem10  43171  fourierdlem42  43203  fourierdlem47  43207  fourierdlem72  43232  fourierdlem79  43239  fourierdlem93  43253  fourierdlem101  43261  fourierdlem103  43263  fourierdlem104  43264  fourierdlem111  43271  hoidmv1lelem2  43643  vonioolem2  43732  vonicclem2  43735  p1lep2  44285  fmtnodvds  44489  lighneallem4a  44553