Theorem leadd1dd 11954

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 11934	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
6	1, 5	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  (class class class)co 7440  ℝcr 11223   + caddc 11227   ≤ cle 11368

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-er 8742  df-en 8999  df-dom 9000  df-sdom 9001  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373

This theorem is used by:  lesub3d  11958  le2addd  11959  supaddc  12308  eluzadd  13018  rpnnen1lem5  13133  xleadd1a  13407  fzoaddel  13876  fladdz  13989  ltdifltdiv  13998  bernneq3  14399  caucvgrlem  15866  eirrlem  16398  vdwlem3  17187  vdwlem9  17193  vdwlem10  17194  2expltfac  17296  psrbagleadd1  22263  pcoass  25372  trirn  25748  minveclem2  25774  ovolfiniun  25849  ovolshftlem1  25857  unmbl  25885  uniioombllem5  25935  opnmbllem  25949  vitalilem2  25957  itg2split  26097  dvfsumlem2  26374  dvfsumlem4  26376  dvfsum2  26381  fta1glem2  26514  coemullem  26596  fta1lem  26655  leibpi  27297  log2tlbnd  27300  jensenlem2  27342  harmonicubnd  27364  harmonicbnd4  27365  lgamgulmlem5  27387  lgambdd  27391  ppiub  27558  bposlem5  27642  mulog2sumlem2  27889  selberg2lem  27904  chpdifbndlem1  27907  pntrlog2bndlem2  27932  pntpbnd2  27941  pntibndlem2  27945  pntlemg  27952  pntlemk  27960  pntlemo  27961  qabvle  27979  ostth2lem3  27989  minvecolem2  31504  nndiffz1  33445  wrdt2ind  33583  cycpmco2lem6  33759  reofld  33971  cos9thpiminplylem1  34481  dya2icoseg  34976  resconn  36177  poimirlem15  38744  opnmbllem0  38765  itg2addnclem3  38782  bfplem2  38948  lcmineqlem19  43288  aks4d1p1p4  43312  aks4d1p1p7  43315  posbezout  43341  sticksstones12  43399  bcle2d  43420  pellexlem2  44028  rmygeid  44162  jm3.1lem2  44216  fzisoeu  46519  absnpncan2d  46521  absnpncan3d  46526  iccshift  46733  fsumnncl  46787  climsuselem1  46822  sumnnodd  46845  climleltrp  46889  dvbdfbdioolem2  47142  ioodvbdlimc1lem1  47144  ioodvbdlimc1lem2  47145  ioodvbdlimc2lem  47147  dvnmul  47156  iblspltprt  47186  itgspltprt  47192  itgiccshift  47193  itgperiod  47194  stoweidlem1  47214  stoweidlem11  47224  stoweidlem14  47227  stoweidlem26  47239  stoweidlem44  47257  stirlinglem11  47297  fourierdlem10  47330  fourierdlem11  47331  fourierdlem15  47335  fourierdlem30  47350  fourierdlem42  47362  fourierdlem68  47387  fourierdlem79  47398  fourierdlem92  47411  sge0xaddlem1  47646  carageniuncllem2  47735  hoidmv1lelem1  47804  ovolval5lem1  47865  smfmullem1  48004