Theorem leadd1dd 11765

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  (class class class)co 7370  ℝcr 11039   + caddc 11043   ≤ cle 11181

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-po 5542  df-so 5543  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186

This theorem is referenced by:  lesub3d  11769  le2addd  11770  supaddc  12123  eluzadd  12794  rpnnen1lem5  12908  xleadd1a  13182  fzoaddel  13647  fladdz  13759  ltdifltdiv  13768  bernneq3  14168  caucvgrlem  15610  eirrlem  16143  vdwlem3  16925  vdwlem9  16931  vdwlem10  16932  2expltfac  17034  psrbagleadd1  21901  pcoass  24997  trirn  25373  minveclem2  25399  ovolfiniun  25475  ovolshftlem1  25483  unmbl  25511  uniioombllem5  25561  opnmbllem  25575  vitalilem2  25583  itg2split  25723  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem4  26009  dvfsum2  26014  fta1glem2  26147  coemullem  26228  fta1lem  26288  leibpi  26925  log2tlbnd  26928  jensenlem2  26971  harmonicubnd  26993  harmonicbnd4  26994  lgamgulmlem5  27016  lgambdd  27020  ppiub  27188  bposlem5  27272  mulog2sumlem2  27519  selberg2lem  27534  chpdifbndlem1  27537  pntrlog2bndlem2  27562  pntpbnd2  27571  pntibndlem2  27575  pntlemg  27582  pntlemk  27590  pntlemo  27591  qabvle  27609  ostth2lem3  27619  minvecolem2  30969  nndiffz1  32883  wrdt2ind  33052  cycpmco2lem6  33231  reofld  33442  cos9thpiminplylem1  33966  dya2icoseg  34461  resconn  35468  poimirlem15  37915  opnmbllem0  37936  itg2addnclem3  37953  bfplem2  38103  lcmineqlem19  42446  aks4d1p1p4  42470  aks4d1p1p7  42473  posbezout  42499  sticksstones12  42557  bcle2d  42578  pellexlem2  43216  rmygeid  43350  jm3.1lem2  43404  fzisoeu  45691  absnpncan2d  45693  absnpncan3d  45698  iccshift  45907  fsumnncl  45961  climsuselem1  45996  sumnnodd  46019  climleltrp  46063  dvbdfbdioolem2  46316  ioodvbdlimc1lem1  46318  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  dvnmul  46330  iblspltprt  46360  itgspltprt  46366  itgiccshift  46367  itgperiod  46368  stoweidlem1  46388  stoweidlem11  46398  stoweidlem14  46401  stoweidlem26  46413  stoweidlem44  46431  stirlinglem11  46471  fourierdlem10  46504  fourierdlem11  46505  fourierdlem15  46509  fourierdlem30  46524  fourierdlem42  46536  fourierdlem68  46561  fourierdlem79  46572  fourierdlem92  46585  sge0xaddlem1  46820  carageniuncllem2  46909  hoidmv1lelem1  46978  ovolval5lem1  47039  smfmullem1  47178