Theorem readdcli 11259

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

Syntax hints:   ∈ wcel 2098  (class class class)co 7417  ℝcr 11137   + caddc 11141

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

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

This theorem is referenced by:  resubcli  11552  eqneg  11964  ledivp1i  12169  ltdivp1i  12170  nnne0  12276  2re  12316  3re  12322  4re  12326  5re  12329  6re  12332  7re  12335  8re  12338  9re  12341  10re  12726  numltc  12733  nn0opthlem2  14260  hashunlei  14416  hashge2el2dif  14473  abs3lemi  15389  ef01bndlem  16160  divalglem6  16374  log2ub  26911  mumullem2  27142  bposlem8  27254  dchrvmasumlem2  27461  ex-fl  30313  norm-ii-i  31003  norm3lem  31015  nmoptrii  31960  bdophsi  31962  unierri  31970  staddi  32112  stadd3i  32114  dp2ltc  32667  dpmul4  32694  ballotlem2  34178  hgt750lem  34353  poimirlem16  37179  itg2addnclem3  37216  fdc  37288  remul02  42025  sn-0tie0  42059  pellqrex  42364  stirlinglem11  45535  fouriersw  45682  zm1nn  46745  evengpoap3  47202