Theorem readdcli 11130

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008   + caddc 11012

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

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

This theorem is referenced by:  resubcli  11426  eqneg  11844  ledivp1i  12050  ltdivp1i  12051  nnne0  12162  2re  12202  3re  12208  4re  12212  5re  12215  6re  12218  7re  12221  8re  12224  9re  12227  10re  12610  numltc  12617  nn0opthlem2  14176  hashunlei  14332  hashge2el2dif  14387  abs3lemi  15318  ef01bndlem  16093  divalglem6  16309  log2ub  26857  mumullem2  27088  bposlem8  27200  dchrvmasumlem2  27407  ex-fl  30391  norm-ii-i  31081  norm3lem  31093  nmoptrii  32038  bdophsi  32040  unierri  32048  staddi  32190  stadd3i  32192  dp2ltc  32828  dpmul4  32855  ballotlem2  34463  hgt750lem  34625  poimirlem16  37626  itg2addnclem3  37663  fdc  37735  remul02  42388  sn-0tie0  42434  pellqrex  42862  stirlinglem11  46075  fouriersw  46222  zm1nn  47296  evengpoap3  47793