Theorem leadd1dd 11690

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5092  (class class class)co 7337  ℝcr 10971   + caddc 10975   ≤ cle 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-po 5532  df-so 5533  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-ov 7340  df-er 8569  df-en 8805  df-dom 8806  df-sdom 8807  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116

This theorem is referenced by:  lesub3d  11694  supaddc  12043  rpnnen1lem5  12822  xleadd1a  13088  fzoaddel  13541  fladdz  13646  ltdifltdiv  13655  bernneq3  14047  caucvgrlem  15483  eirrlem  16012  vdwlem3  16781  vdwlem9  16787  vdwlem10  16788  2expltfac  16891  pcoass  24293  trirn  24670  minveclem2  24696  ovolfiniun  24771  ovolshftlem1  24779  unmbl  24807  uniioombllem5  24857  opnmbllem  24871  vitalilem2  24879  itg2split  25020  dvfsumlem2  25297  dvfsumlem4  25299  dvfsum2  25304  fta1glem2  25437  coemullem  25517  fta1lem  25573  leibpi  26198  log2tlbnd  26201  jensenlem2  26243  harmonicubnd  26265  harmonicbnd4  26266  lgamgulmlem5  26288  lgambdd  26292  ppiub  26458  bposlem5  26542  mulog2sumlem2  26789  selberg2lem  26804  chpdifbndlem1  26807  pntrlog2bndlem2  26832  pntpbnd2  26841  pntibndlem2  26845  pntlemg  26852  pntlemk  26860  pntlemo  26861  qabvle  26879  ostth2lem3  26889  minvecolem2  29525  nndiffz1  31394  wrdt2ind  31512  cycpmco2lem6  31685  reofld  31840  dya2icoseg  32544  resconn  33507  poimirlem15  35905  opnmbllem0  35926  itg2addnclem3  35943  bfplem2  36094  lcmineqlem19  40317  aks4d1p1p4  40341  aks4d1p1p7  40344  sticksstones12  40379  metakunt2  40391  pellexlem2  40922  rmygeid  41057  jm3.1lem2  41111  fzisoeu  43182  absnpncan2d  43184  absnpncan3d  43189  leadd12dd  43198  iccshift  43400  fsumnncl  43457  climsuselem1  43492  sumnnodd  43515  climleltrp  43561  dvbdfbdioolem2  43814  ioodvbdlimc1lem1  43816  ioodvbdlimc1lem2  43817  ioodvbdlimc2lem  43819  dvnmul  43828  iblspltprt  43858  itgspltprt  43864  itgiccshift  43865  itgperiod  43866  stoweidlem1  43886  stoweidlem11  43896  stoweidlem14  43899  stoweidlem26  43911  stoweidlem44  43929  stirlinglem11  43969  fourierdlem10  44002  fourierdlem11  44003  fourierdlem15  44007  fourierdlem30  44022  fourierdlem42  44034  fourierdlem68  44059  fourierdlem79  44070  fourierdlem92  44083  sge0xaddlem1  44316  carageniuncllem2  44405  hoidmv1lelem1  44474  ovolval5lem1  44535  smfmullem1  44674