Theorem leadd1dd 11755

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5099  (class class class)co 7360  ℝcr 11029   + caddc 11033   ≤ cle 11171

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106

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 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  lesub3d  11759  le2addd  11760  supaddc  12113  eluzadd  12784  rpnnen1lem5  12898  xleadd1a  13172  fzoaddel  13637  fladdz  13749  ltdifltdiv  13758  bernneq3  14158  caucvgrlem  15600  eirrlem  16133  vdwlem3  16915  vdwlem9  16921  vdwlem10  16922  2expltfac  17024  psrbagleadd1  21888  pcoass  24984  trirn  25360  minveclem2  25386  ovolfiniun  25462  ovolshftlem1  25470  unmbl  25498  uniioombllem5  25548  opnmbllem  25562  vitalilem2  25570  itg2split  25710  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem4  25996  dvfsum2  26001  fta1glem2  26134  coemullem  26215  fta1lem  26275  leibpi  26912  log2tlbnd  26915  jensenlem2  26958  harmonicubnd  26980  harmonicbnd4  26981  lgamgulmlem5  27003  lgambdd  27007  ppiub  27175  bposlem5  27259  mulog2sumlem2  27506  selberg2lem  27521  chpdifbndlem1  27524  pntrlog2bndlem2  27549  pntpbnd2  27558  pntibndlem2  27562  pntlemg  27569  pntlemk  27577  pntlemo  27578  qabvle  27596  ostth2lem3  27606  minvecolem2  30954  nndiffz1  32868  wrdt2ind  33037  cycpmco2lem6  33215  reofld  33426  cos9thpiminplylem1  33941  dya2icoseg  34436  resconn  35442  poimirlem15  37838  opnmbllem0  37859  itg2addnclem3  37876  bfplem2  38026  lcmineqlem19  42369  aks4d1p1p4  42393  aks4d1p1p7  42396  posbezout  42422  sticksstones12  42480  bcle2d  42501  pellexlem2  43139  rmygeid  43273  jm3.1lem2  43327  fzisoeu  45615  absnpncan2d  45617  absnpncan3d  45622  iccshift  45831  fsumnncl  45885  climsuselem1  45920  sumnnodd  45943  climleltrp  45987  dvbdfbdioolem2  46240  ioodvbdlimc1lem1  46242  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  dvnmul  46254  iblspltprt  46284  itgspltprt  46290  itgiccshift  46291  itgperiod  46292  stoweidlem1  46312  stoweidlem11  46322  stoweidlem14  46325  stoweidlem26  46337  stoweidlem44  46355  stirlinglem11  46395  fourierdlem10  46428  fourierdlem11  46429  fourierdlem15  46433  fourierdlem30  46448  fourierdlem42  46460  fourierdlem68  46485  fourierdlem79  46496  fourierdlem92  46509  sge0xaddlem1  46744  carageniuncllem2  46833  hoidmv1lelem1  46902  ovolval5lem1  46963  smfmullem1  47102