Theorem leadd1dd 11803

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

Syntax hints:   → wi 4   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7398  ℝcr 11074   + caddc 11078   ≤ cle 11219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-po 5557  df-so 5558  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7401  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224

This theorem is referenced by:  lesub3d  11807  le2addd  11808  supaddc  12161  eluzadd  12870  rpnnen1lem5  12984  xleadd1a  13258  fzoaddel  13725  fladdz  13837  ltdifltdiv  13846  bernneq3  14246  caucvgrlem  15702  eirrlem  16238  vdwlem3  17021  vdwlem9  17027  vdwlem10  17028  2expltfac  17130  psrbagleadd1  21982  pcoass  25088  trirn  25464  minveclem2  25490  ovolfiniun  25565  ovolshftlem1  25573  unmbl  25601  uniioombllem5  25651  opnmbllem  25665  vitalilem2  25673  itg2split  25813  dvfsumlem2  26091  dvfsumlem4  26093  dvfsum2  26098  fta1glem2  26231  coemullem  26312  fta1lem  26373  leibpi  27009  log2tlbnd  27012  jensenlem2  27054  harmonicubnd  27076  harmonicbnd4  27077  lgamgulmlem5  27099  lgambdd  27103  ppiub  27270  bposlem5  27354  mulog2sumlem2  27601  selberg2lem  27616  chpdifbndlem1  27619  pntrlog2bndlem2  27644  pntpbnd2  27653  pntibndlem2  27657  pntlemg  27664  pntlemk  27672  pntlemo  27673  qabvle  27691  ostth2lem3  27701  minvecolem2  31080  nndiffz1  32990  wrdt2ind  33133  cycpmco2lem6  33313  reofld  33531  cos9thpiminplylem1  34081  dya2icoseg  34576  resconn  35601  poimirlem15  38139  opnmbllem0  38160  itg2addnclem3  38177  bfplem2  38327  lcmineqlem19  42669  aks4d1p1p4  42693  aks4d1p1p7  42696  posbezout  42722  sticksstones12  42780  bcle2d  42801  pellexlem2  43412  rmygeid  43546  jm3.1lem2  43600  fzisoeu  45884  absnpncan2d  45886  absnpncan3d  45891  iccshift  46099  fsumnncl  46153  climsuselem1  46188  sumnnodd  46211  climleltrp  46255  dvbdfbdioolem2  46508  ioodvbdlimc1lem1  46510  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  dvnmul  46522  iblspltprt  46552  itgspltprt  46558  itgiccshift  46559  itgperiod  46560  stoweidlem1  46580  stoweidlem11  46590  stoweidlem14  46593  stoweidlem26  46605  stoweidlem44  46623  stirlinglem11  46663  fourierdlem10  46696  fourierdlem11  46697  fourierdlem15  46701  fourierdlem30  46716  fourierdlem42  46728  fourierdlem68  46753  fourierdlem79  46764  fourierdlem92  46777  sge0xaddlem1  47012  carageniuncllem2  47101  hoidmv1lelem1  47170  ovolval5lem1  47231  smfmullem1  47370