Theorem leadd1dd 11853

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
leadd1dd	⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))

Proof of Theorem leadd1dd

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  (class class class)co 7416  ℝcr 11124   + caddc 11128   ≤ cle 11269

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274

This theorem is used by:  lesub3d  11857  le2addd  11858  supaddc  12207  eluzadd  12917  rpnnen1lem5  13031  xleadd1a  13305  fzoaddel  13773  fladdz  13886  ltdifltdiv  13895  bernneq3  14295  caucvgrlem  15760  eirrlem  16294  vdwlem3  17077  vdwlem9  17083  vdwlem10  17084  2expltfac  17186  psrbagleadd1  22142  pcoass  25251  trirn  25627  minveclem2  25653  ovolfiniun  25728  ovolshftlem1  25736  unmbl  25764  uniioombllem5  25814  opnmbllem  25828  vitalilem2  25836  itg2split  25976  dvfsumlem2  26254  dvfsumlem4  26256  dvfsum2  26261  fta1glem2  26394  coemullem  26475  fta1lem  26536  leibpi  27175  log2tlbnd  27178  jensenlem2  27220  harmonicubnd  27242  harmonicbnd4  27243  lgamgulmlem5  27265  lgambdd  27269  ppiub  27436  bposlem5  27520  mulog2sumlem2  27767  selberg2lem  27782  chpdifbndlem1  27785  pntrlog2bndlem2  27810  pntpbnd2  27819  pntibndlem2  27823  pntlemg  27830  pntlemk  27838  pntlemo  27839  qabvle  27857  ostth2lem3  27867  minvecolem2  31340  nndiffz1  33242  wrdt2ind  33380  cycpmco2lem6  33556  reofld  33768  cos9thpiminplylem1  34277  dya2icoseg  34773  resconn  35810  poimirlem15  38369  opnmbllem0  38390  itg2addnclem3  38407  bfplem2  38558  lcmineqlem19  42898  aks4d1p1p4  42922  aks4d1p1p7  42925  posbezout  42951  sticksstones12  43009  bcle2d  43030  pellexlem2  43656  rmygeid  43790  jm3.1lem2  43844  fzisoeu  46118  absnpncan2d  46120  absnpncan3d  46125  iccshift  46333  fsumnncl  46387  climsuselem1  46422  sumnnodd  46445  climleltrp  46489  dvbdfbdioolem2  46742  ioodvbdlimc1lem1  46744  ioodvbdlimc1lem2  46745  ioodvbdlimc2lem  46747  dvnmul  46756  iblspltprt  46786  itgspltprt  46792  itgiccshift  46793  itgperiod  46794  stoweidlem1  46814  stoweidlem11  46824  stoweidlem14  46827  stoweidlem26  46839  stoweidlem44  46857  stirlinglem11  46897  fourierdlem10  46930  fourierdlem11  46931  fourierdlem15  46935  fourierdlem30  46950  fourierdlem42  46962  fourierdlem68  46987  fourierdlem79  46998  fourierdlem92  47011  sge0xaddlem1  47246  carageniuncllem2  47335  hoidmv1lelem1  47404  ovolval5lem1  47465  smfmullem1  47604