Theorem readdcli 10659

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 10623	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 690	1 ⊢ (𝐴 + 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7159  ℝcr 10539   + caddc 10543

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  resubcli  10951  eqneg  11363  ledivp1i  11568  ltdivp1i  11569  nnne0  11674  2re  11714  3re  11720  4re  11724  5re  11727  6re  11730  7re  11733  8re  11736  9re  11739  10re  12120  numltc  12127  nn0opthlem2  13632  hashunlei  13789  hashge2el2dif  13841  abs3lemi  14773  ef01bndlem  15540  divalglem6  15752  log2ub  25530  mumullem2  25760  bposlem8  25870  dchrvmasumlem2  26077  ex-fl  28229  norm-ii-i  28917  norm3lem  28929  nmoptrii  29874  bdophsi  29876  unierri  29884  staddi  30026  stadd3i  30028  dp2ltc  30567  dpmul4  30594  ballotlem2  31750  hgt750lem  31926  poimirlem16  34912  itg2addnclem3  34949  fdc  35024  remul02  39241  pellqrex  39482  stirlinglem11  42376  fouriersw  42523  zm1nn  43509  evengpoap3  43971