Theorem leadd1dd 11768

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  (class class class)co 7369  ℝcr 11043   + caddc 11047   ≤ cle 11185

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120

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 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lesub3d  11772  le2addd  11773  supaddc  12126  eluzadd  12798  rpnnen1lem5  12916  xleadd1a  13189  fzoaddel  13654  fladdz  13763  ltdifltdiv  13772  bernneq3  14172  caucvgrlem  15615  eirrlem  16148  vdwlem3  16930  vdwlem9  16936  vdwlem10  16937  2expltfac  17039  psrbagleadd1  21870  pcoass  24957  trirn  25333  minveclem2  25359  ovolfiniun  25435  ovolshftlem1  25443  unmbl  25471  uniioombllem5  25521  opnmbllem  25535  vitalilem2  25543  itg2split  25683  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem4  25969  dvfsum2  25974  fta1glem2  26107  coemullem  26188  fta1lem  26248  leibpi  26885  log2tlbnd  26888  jensenlem2  26931  harmonicubnd  26953  harmonicbnd4  26954  lgamgulmlem5  26976  lgambdd  26980  ppiub  27148  bposlem5  27232  mulog2sumlem2  27479  selberg2lem  27494  chpdifbndlem1  27497  pntrlog2bndlem2  27522  pntpbnd2  27531  pntibndlem2  27535  pntlemg  27542  pntlemk  27550  pntlemo  27551  qabvle  27569  ostth2lem3  27579  minvecolem2  30854  nndiffz1  32759  wrdt2ind  32925  cycpmco2lem6  33103  reofld  33308  cos9thpiminplylem1  33765  dya2icoseg  34261  resconn  35226  poimirlem15  37622  opnmbllem0  37643  itg2addnclem3  37660  bfplem2  37810  lcmineqlem19  42028  aks4d1p1p4  42052  aks4d1p1p7  42055  posbezout  42081  sticksstones12  42139  bcle2d  42160  pellexlem2  42811  rmygeid  42946  jm3.1lem2  43000  fzisoeu  45291  absnpncan2d  45293  absnpncan3d  45298  iccshift  45509  fsumnncl  45563  climsuselem1  45598  sumnnodd  45621  climleltrp  45667  dvbdfbdioolem2  45920  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  iblspltprt  45964  itgspltprt  45970  itgiccshift  45971  itgperiod  45972  stoweidlem1  45992  stoweidlem11  46002  stoweidlem14  46005  stoweidlem26  46017  stoweidlem44  46035  stirlinglem11  46075  fourierdlem10  46108  fourierdlem11  46109  fourierdlem15  46113  fourierdlem30  46128  fourierdlem42  46140  fourierdlem68  46165  fourierdlem79  46176  fourierdlem92  46189  sge0xaddlem1  46424  carageniuncllem2  46513  hoidmv1lelem1  46582  ovolval5lem1  46643  smfmullem1  46782