Theorem readdcli 10694

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7150  ℝcr 10574   + caddc 10578

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

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

This theorem is referenced by:  resubcli  10986  eqneg  11398  ledivp1i  11603  ltdivp1i  11604  nnne0  11708  2re  11748  3re  11754  4re  11758  5re  11761  6re  11764  7re  11767  8re  11770  9re  11773  10re  12156  numltc  12163  nn0opthlem2  13679  hashunlei  13836  hashge2el2dif  13890  abs3lemi  14818  ef01bndlem  15585  divalglem6  15799  log2ub  25634  mumullem2  25864  bposlem8  25974  dchrvmasumlem2  26181  ex-fl  28331  norm-ii-i  29019  norm3lem  29031  nmoptrii  29976  bdophsi  29978  unierri  29986  staddi  30128  stadd3i  30130  dp2ltc  30685  dpmul4  30712  ballotlem2  31974  hgt750lem  32150  poimirlem16  35353  itg2addnclem3  35390  fdc  35463  remul02  39885  sn-0tie0  39918  pellqrex  40193  stirlinglem11  43092  fouriersw  43239  zm1nn  44227  evengpoap3  44684