Theorem readdcli 10266

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

Syntax hints:   ∈ wcel 2140  (class class class)co 6815  ℝcr 10148   + caddc 10152

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

This theorem depends on definitions:  df-bi 197  df-an 385

This theorem is referenced by:  resubcli  10556  eqneg  10958  ledivp1i  11162  ltdivp1i  11163  2re  11303  3re  11307  4re  11310  5re  11312  6re  11314  7re  11316  8re  11318  9re  11320  10reOLD  11322  numltc  11741  nn0opthlem2  13271  hashunlei  13425  hashge2el2dif  13475  abs3lemi  14369  ef01bndlem  15134  divalglem6  15344  log2ub  24897  mumullem2  25127  bposlem8  25237  dchrvmasumlem2  25408  ex-fl  27637  norm-ii-i  28325  norm3lem  28337  nmoptrii  29284  bdophsi  29286  unierri  29294  staddi  29436  stadd3i  29438  dp2ltc  29925  dpmul4  29953  ballotlem2  30881  hgt750lem  31060  poimirlem16  33757  itg2addnclem3  33795  fdc  33873  pellqrex  37964  stirlinglem11  40823  fouriersw  40970  zm1nn  41845  evengpoap3  42216