Theorem leadd1dd 11830

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  (class class class)co 7411  ℝcr 11111   + caddc 11115   ≤ cle 11251

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256

This theorem is referenced by:  lesub3d  11834  supaddc  12183  eluzadd  12853  rpnnen1lem5  12967  xleadd1a  13234  fzoaddel  13687  fladdz  13792  ltdifltdiv  13801  bernneq3  14196  caucvgrlem  15621  eirrlem  16149  vdwlem3  16918  vdwlem9  16924  vdwlem10  16925  2expltfac  17028  pcoass  24547  trirn  24924  minveclem2  24950  ovolfiniun  25025  ovolshftlem1  25033  unmbl  25061  uniioombllem5  25111  opnmbllem  25125  vitalilem2  25133  itg2split  25274  dvfsumlem2  25551  dvfsumlem4  25553  dvfsum2  25558  fta1glem2  25691  coemullem  25771  fta1lem  25827  leibpi  26454  log2tlbnd  26457  jensenlem2  26499  harmonicubnd  26521  harmonicbnd4  26522  lgamgulmlem5  26544  lgambdd  26548  ppiub  26714  bposlem5  26798  mulog2sumlem2  27045  selberg2lem  27060  chpdifbndlem1  27063  pntrlog2bndlem2  27088  pntpbnd2  27097  pntibndlem2  27101  pntlemg  27108  pntlemk  27116  pntlemo  27117  qabvle  27135  ostth2lem3  27145  minvecolem2  30166  nndiffz1  32035  wrdt2ind  32155  cycpmco2lem6  32331  reofld  32500  dya2icoseg  33345  resconn  34306  gg-dvfsumlem2  35252  poimirlem15  36589  opnmbllem0  36610  itg2addnclem3  36627  bfplem2  36777  lcmineqlem19  40998  aks4d1p1p4  41022  aks4d1p1p7  41025  sticksstones12  41060  metakunt2  41072  pellexlem2  41650  rmygeid  41785  jm3.1lem2  41839  fzisoeu  44089  absnpncan2d  44091  absnpncan3d  44096  leadd12dd  44105  iccshift  44310  fsumnncl  44367  climsuselem1  44402  sumnnodd  44425  climleltrp  44471  dvbdfbdioolem2  44724  ioodvbdlimc1lem1  44726  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnmul  44738  iblspltprt  44768  itgspltprt  44774  itgiccshift  44775  itgperiod  44776  stoweidlem1  44796  stoweidlem11  44806  stoweidlem14  44809  stoweidlem26  44821  stoweidlem44  44839  stirlinglem11  44879  fourierdlem10  44912  fourierdlem11  44913  fourierdlem15  44917  fourierdlem30  44932  fourierdlem42  44944  fourierdlem68  44969  fourierdlem79  44980  fourierdlem92  44993  sge0xaddlem1  45228  carageniuncllem2  45317  hoidmv1lelem1  45386  ovolval5lem1  45447  smfmullem1  45586