Theorem leadd1dd 11877

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7416  ℝcr 11148   + caddc 11152   ≤ cle 11293

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 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  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 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-ov 7419  df-er 8703  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298

This theorem is used by:  lesub3d  11881  le2addd  11882  supaddc  12231  eluzadd  12941  rpnnen1lem5  13056  xleadd1a  13330  fzoaddel  13798  fladdz  13911  ltdifltdiv  13920  bernneq3  14320  caucvgrlem  15785  eirrlem  16317  vdwlem3  17100  vdwlem9  17106  vdwlem10  17107  2expltfac  17209  psrbagleadd1  22175  pcoass  25284  trirn  25660  minveclem2  25686  ovolfiniun  25761  ovolshftlem1  25769  unmbl  25797  uniioombllem5  25847  opnmbllem  25861  vitalilem2  25869  itg2split  26009  dvfsumlem2  26286  dvfsumlem4  26288  dvfsum2  26293  fta1glem2  26426  coemullem  26508  fta1lem  26569  leibpi  27211  log2tlbnd  27214  jensenlem2  27256  harmonicubnd  27278  harmonicbnd4  27279  lgamgulmlem5  27301  lgambdd  27305  ppiub  27472  bposlem5  27556  mulog2sumlem2  27803  selberg2lem  27818  chpdifbndlem1  27821  pntrlog2bndlem2  27846  pntpbnd2  27855  pntibndlem2  27859  pntlemg  27866  pntlemk  27874  pntlemo  27875  qabvle  27893  ostth2lem3  27903  minvecolem2  31388  nndiffz1  33289  wrdt2ind  33427  cycpmco2lem6  33603  reofld  33815  cos9thpiminplylem1  34325  dya2icoseg  34821  resconn  35908  poimirlem15  38449  opnmbllem0  38470  itg2addnclem3  38487  bfplem2  38638  lcmineqlem19  42978  aks4d1p1p4  43002  aks4d1p1p7  43005  posbezout  43031  sticksstones12  43089  bcle2d  43110  pellexlem2  43736  rmygeid  43870  jm3.1lem2  43924  fzisoeu  46198  absnpncan2d  46200  absnpncan3d  46205  iccshift  46413  fsumnncl  46467  climsuselem1  46502  sumnnodd  46525  climleltrp  46569  dvbdfbdioolem2  46822  ioodvbdlimc1lem1  46824  ioodvbdlimc1lem2  46825  ioodvbdlimc2lem  46827  dvnmul  46836  iblspltprt  46866  itgspltprt  46872  itgiccshift  46873  itgperiod  46874  stoweidlem1  46894  stoweidlem11  46904  stoweidlem14  46907  stoweidlem26  46919  stoweidlem44  46937  stirlinglem11  46977  fourierdlem10  47010  fourierdlem11  47011  fourierdlem15  47015  fourierdlem30  47030  fourierdlem42  47042  fourierdlem68  47067  fourierdlem79  47078  fourierdlem92  47091  sge0xaddlem1  47326  carageniuncllem2  47415  hoidmv1lelem1  47484  ovolval5lem1  47545  smfmullem1  47684