Theorem readdcli 11229

Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
readdcli	⊢ (𝐴 + 𝐵) ∈ ℝ

Proof of Theorem readdcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		readdcl 11193	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 + 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109   + caddc 11113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11171

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  resubcli  11522  eqneg  11934  ledivp1i  12139  ltdivp1i  12140  nnne0  12246  2re  12286  3re  12292  4re  12296  5re  12299  6re  12302  7re  12305  8re  12308  9re  12311  10re  12696  numltc  12703  nn0opthlem2  14229  hashunlei  14385  hashge2el2dif  14441  abs3lemi  15357  ef01bndlem  16127  divalglem6  16341  log2ub  26454  mumullem2  26684  bposlem8  26794  dchrvmasumlem2  27001  ex-fl  29700  norm-ii-i  30390  norm3lem  30402  nmoptrii  31347  bdophsi  31349  unierri  31357  staddi  31499  stadd3i  31501  dp2ltc  32053  dpmul4  32080  ballotlem2  33487  hgt750lem  33663  poimirlem16  36504  itg2addnclem3  36541  fdc  36613  remul02  41278  sn-0tie0  41312  pellqrex  41617  stirlinglem11  44800  fouriersw  44947  zm1nn  46010  evengpoap3  46467