Theorem readdcli 9932

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

Syntax hints:   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814   + caddc 9818

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

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

This theorem is referenced by:  resubcli  10222  eqneg  10624  ledivp1i  10828  ltdivp1i  10829  2re  10967  3re  10971  4re  10974  5re  10976  6re  10978  7re  10980  8re  10982  9re  10984  10reOLD  10986  numltc  11404  nn0opthlem2  12918  hashunlei  13072  hashge2el2dif  13117  abs3lemi  13997  ef01bndlem  14753  divalglem6  14959  log2ub  24476  mumullem2  24706  bposlem8  24816  dchrvmasumlem2  24987  ex-fl  26696  norm-ii-i  27378  norm3lem  27390  nmoptrii  28337  bdophsi  28339  unierri  28347  staddi  28489  stadd3i  28491  ballotlem2  29877  poimirlem16  32595  itg2addnclem3  32633  fdc  32711  pellqrex  36461  stirlinglem11  38977  fouriersw  39124  evengpoap3  40215  zm1nn  40348