Theorem readdcli 10656

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536   + caddc 10540

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

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

This theorem is referenced by:  resubcli  10948  eqneg  11360  ledivp1i  11565  ltdivp1i  11566  nnne0  11672  2re  11712  3re  11718  4re  11722  5re  11725  6re  11728  7re  11731  8re  11734  9re  11737  10re  12118  numltc  12125  nn0opthlem2  13630  hashunlei  13787  hashge2el2dif  13839  abs3lemi  14770  ef01bndlem  15537  divalglem6  15749  log2ub  25527  mumullem2  25757  bposlem8  25867  dchrvmasumlem2  26074  ex-fl  28226  norm-ii-i  28914  norm3lem  28926  nmoptrii  29871  bdophsi  29873  unierri  29881  staddi  30023  stadd3i  30025  dp2ltc  30563  dpmul4  30590  ballotlem2  31746  hgt750lem  31922  poimirlem16  34923  itg2addnclem3  34960  fdc  35035  remul02  39255  pellqrex  39496  stirlinglem11  42389  fouriersw  42536  zm1nn  43522  evengpoap3  43984