Theorem readdcli 11219

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

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094   + caddc 11098

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  resubcli  11515  eqneg  11930  ledivp1i  12135  ltdivp1i  12136  nnne0  12265  2re  12310  3re  12316  4re  12320  5re  12323  6re  12326  7re  12329  8re  12332  9re  12335  10re  12729  numltc  12737  nn0opthlem2  14301  hashunlei  14458  hashge2el2dif  14513  abs3lemi  15458  ef01bndlem  16235  divalglem6  16451  log2ub  27114  mumullem2  27344  bposlem8  27455  dchrvmasumlem2  27662  ex-fl  30798  norm-ii-i  31489  norm3lem  31501  nmoptrii  32446  bdophsi  32448  unierri  32456  staddi  32598  stadd3i  32600  dp2ltc  33206  dpmul4  33233  ballotlem2  34879  hgt750lem  35038  poimirlem16  38307  itg2addnclem3  38344  fdc  38416  remul02  43186  sn-0tie0  43245  pellqrex  43626  stirlinglem11  46818  fouriersw  46965  zm1nn  48059  evengpoap3  48584  crossp3i  50668