Theorem leadd1dd 11792

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5107  (class class class)co 7387  ℝcr 11067   + caddc 11071   ≤ cle 11209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-po 5546  df-so 5547  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  lesub3d  11796  le2addd  11797  supaddc  12150  eluzadd  12822  rpnnen1lem5  12940  xleadd1a  13213  fzoaddel  13678  fladdz  13787  ltdifltdiv  13796  bernneq3  14196  caucvgrlem  15639  eirrlem  16172  vdwlem3  16954  vdwlem9  16960  vdwlem10  16961  2expltfac  17063  psrbagleadd1  21837  pcoass  24924  trirn  25300  minveclem2  25326  ovolfiniun  25402  ovolshftlem1  25410  unmbl  25438  uniioombllem5  25488  opnmbllem  25502  vitalilem2  25510  itg2split  25650  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsum2  25941  fta1glem2  26074  coemullem  26155  fta1lem  26215  leibpi  26852  log2tlbnd  26855  jensenlem2  26898  harmonicubnd  26920  harmonicbnd4  26921  lgamgulmlem5  26943  lgambdd  26947  ppiub  27115  bposlem5  27199  mulog2sumlem2  27446  selberg2lem  27461  chpdifbndlem1  27464  pntrlog2bndlem2  27489  pntpbnd2  27498  pntibndlem2  27502  pntlemg  27509  pntlemk  27517  pntlemo  27518  qabvle  27536  ostth2lem3  27546  minvecolem2  30804  nndiffz1  32709  wrdt2ind  32875  cycpmco2lem6  33088  reofld  33315  cos9thpiminplylem1  33772  dya2icoseg  34268  resconn  35233  poimirlem15  37629  opnmbllem0  37650  itg2addnclem3  37667  bfplem2  37817  lcmineqlem19  42035  aks4d1p1p4  42059  aks4d1p1p7  42062  posbezout  42088  sticksstones12  42146  bcle2d  42167  pellexlem2  42818  rmygeid  42953  jm3.1lem2  43007  fzisoeu  45298  absnpncan2d  45300  absnpncan3d  45305  iccshift  45516  fsumnncl  45570  climsuselem1  45605  sumnnodd  45628  climleltrp  45674  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  itgiccshift  45978  itgperiod  45979  stoweidlem1  45999  stoweidlem11  46009  stoweidlem14  46012  stoweidlem26  46024  stoweidlem44  46042  stirlinglem11  46082  fourierdlem10  46115  fourierdlem11  46116  fourierdlem15  46120  fourierdlem30  46135  fourierdlem42  46147  fourierdlem68  46172  fourierdlem79  46183  fourierdlem92  46196  sge0xaddlem1  46431  carageniuncllem2  46520  hoidmv1lelem1  46589  ovolval5lem1  46650  smfmullem1  46789