Theorem leadd1dd 11878

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

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5153  (class class class)co 7424  ℝcr 11157   + caddc 11161   ≤ cle 11299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304

This theorem is referenced by:  lesub3d  11882  supaddc  12233  eluzadd  12903  rpnnen1lem5  13017  xleadd1a  13286  fzoaddel  13739  fladdz  13845  ltdifltdiv  13854  bernneq3  14248  caucvgrlem  15677  eirrlem  16206  vdwlem3  16985  vdwlem9  16991  vdwlem10  16992  2expltfac  17095  psrbagleadd1  21933  pcoass  25042  trirn  25419  minveclem2  25445  ovolfiniun  25521  ovolshftlem1  25529  unmbl  25557  uniioombllem5  25607  opnmbllem  25621  vitalilem2  25629  itg2split  25770  dvfsumlem2  26052  dvfsumlem2OLD  26053  dvfsumlem4  26055  dvfsum2  26060  fta1glem2  26196  coemullem  26277  fta1lem  26335  leibpi  26970  log2tlbnd  26973  jensenlem2  27016  harmonicubnd  27038  harmonicbnd4  27039  lgamgulmlem5  27061  lgambdd  27065  ppiub  27233  bposlem5  27317  mulog2sumlem2  27564  selberg2lem  27579  chpdifbndlem1  27582  pntrlog2bndlem2  27607  pntpbnd2  27616  pntibndlem2  27620  pntlemg  27627  pntlemk  27635  pntlemo  27636  qabvle  27654  ostth2lem3  27664  minvecolem2  30808  nndiffz1  32688  wrdt2ind  32817  cycpmco2lem6  33009  reofld  33219  dya2icoseg  34111  resconn  35074  poimirlem15  37336  opnmbllem0  37357  itg2addnclem3  37374  bfplem2  37524  lcmineqlem19  41746  aks4d1p1p4  41770  aks4d1p1p7  41773  posbezout  41798  sticksstones12  41856  bcle2d  41877  metakunt2  41892  pellexlem2  42487  rmygeid  42622  jm3.1lem2  42676  fzisoeu  44915  absnpncan2d  44917  absnpncan3d  44922  leadd12dd  44931  iccshift  45136  fsumnncl  45193  climsuselem1  45228  sumnnodd  45251  climleltrp  45297  dvbdfbdioolem2  45550  ioodvbdlimc1lem1  45552  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  dvnmul  45564  iblspltprt  45594  itgspltprt  45600  itgiccshift  45601  itgperiod  45602  stoweidlem1  45622  stoweidlem11  45632  stoweidlem14  45635  stoweidlem26  45647  stoweidlem44  45665  stirlinglem11  45705  fourierdlem10  45738  fourierdlem11  45739  fourierdlem15  45743  fourierdlem30  45758  fourierdlem42  45770  fourierdlem68  45795  fourierdlem79  45806  fourierdlem92  45819  sge0xaddlem1  46054  carageniuncllem2  46143  hoidmv1lelem1  46212  ovolval5lem1  46273  smfmullem1  46412