Theorem readdcli 11145

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023   + caddc 11027

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  resubcli  11441  eqneg  11859  ledivp1i  12065  ltdivp1i  12066  nnne0  12177  2re  12217  3re  12223  4re  12227  5re  12230  6re  12233  7re  12236  8re  12239  9re  12242  10re  12624  numltc  12631  nn0opthlem2  14190  hashunlei  14346  hashge2el2dif  14401  abs3lemi  15332  ef01bndlem  16107  divalglem6  16323  log2ub  26913  mumullem2  27144  bposlem8  27256  dchrvmasumlem2  27463  ex-fl  30471  norm-ii-i  31161  norm3lem  31173  nmoptrii  32118  bdophsi  32120  unierri  32128  staddi  32270  stadd3i  32272  dp2ltc  32917  dpmul4  32944  ballotlem2  34595  hgt750lem  34757  poimirlem16  37776  itg2addnclem3  37813  fdc  37885  remul02  42602  sn-0tie0  42648  pellqrex  43063  stirlinglem11  46270  fouriersw  46417  zm1nn  47490  evengpoap3  47987