Theorem leadd1dd 11832

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410  ℝcr 11103   + caddc 11107   ≤ cle 11248

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253

This theorem is used by:  lesub3d  11836  le2addd  11837  supaddc  12186  eluzadd  12895  rpnnen1lem5  13009  xleadd1a  13283  fzoaddel  13751  fladdz  13863  ltdifltdiv  13872  bernneq3  14272  caucvgrlem  15729  eirrlem  16264  vdwlem3  17047  vdwlem9  17053  vdwlem10  17054  2expltfac  17156  psrbagleadd1  22087  pcoass  25192  trirn  25568  minveclem2  25594  ovolfiniun  25669  ovolshftlem1  25677  unmbl  25705  uniioombllem5  25755  opnmbllem  25769  vitalilem2  25777  itg2split  25917  dvfsumlem2  26195  dvfsumlem4  26197  dvfsum2  26202  fta1glem2  26335  coemullem  26416  fta1lem  26477  leibpi  27116  log2tlbnd  27119  jensenlem2  27161  harmonicubnd  27183  harmonicbnd4  27184  lgamgulmlem5  27206  lgambdd  27210  ppiub  27377  bposlem5  27461  mulog2sumlem2  27708  selberg2lem  27723  chpdifbndlem1  27726  pntrlog2bndlem2  27751  pntpbnd2  27760  pntibndlem2  27764  pntlemg  27771  pntlemk  27779  pntlemo  27780  qabvle  27798  ostth2lem3  27808  minvecolem2  31236  nndiffz1  33140  wrdt2ind  33282  cycpmco2lem6  33460  reofld  33672  cos9thpiminplylem1  34181  dya2icoseg  34676  resconn  35746  poimirlem15  38314  opnmbllem0  38335  itg2addnclem3  38352  bfplem2  38502  lcmineqlem19  42842  aks4d1p1p4  42866  aks4d1p1p7  42869  posbezout  42895  sticksstones12  42953  bcle2d  42974  pellexlem2  43585  rmygeid  43719  jm3.1lem2  43773  fzisoeu  46047  absnpncan2d  46049  absnpncan3d  46054  iccshift  46262  fsumnncl  46316  climsuselem1  46351  sumnnodd  46374  climleltrp  46418  dvbdfbdioolem2  46671  ioodvbdlimc1lem1  46673  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  dvnmul  46685  iblspltprt  46715  itgspltprt  46721  itgiccshift  46722  itgperiod  46723  stoweidlem1  46743  stoweidlem11  46753  stoweidlem14  46756  stoweidlem26  46768  stoweidlem44  46786  stirlinglem11  46826  fourierdlem10  46859  fourierdlem11  46860  fourierdlem15  46864  fourierdlem30  46879  fourierdlem42  46891  fourierdlem68  46916  fourierdlem79  46927  fourierdlem92  46940  sge0xaddlem1  47175  carageniuncllem2  47264  hoidmv1lelem1  47333  ovolval5lem1  47394  smfmullem1  47533