Theorem readdcli 11160

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037   + caddc 11041

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

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

This theorem is referenced by:  resubcli  11456  eqneg  11875  ledivp1i  12081  ltdivp1i  12082  nnne0  12211  2re  12255  3re  12261  4re  12265  5re  12268  6re  12271  7re  12274  8re  12277  9re  12280  10re  12663  numltc  12670  nn0opthlem2  14231  hashunlei  14387  hashge2el2dif  14442  abs3lemi  15373  ef01bndlem  16151  divalglem6  16367  log2ub  26913  mumullem2  27143  bposlem8  27254  dchrvmasumlem2  27461  ex-fl  30517  norm-ii-i  31208  norm3lem  31220  nmoptrii  32165  bdophsi  32167  unierri  32175  staddi  32317  stadd3i  32319  dp2ltc  32946  dpmul4  32973  ballotlem2  34633  hgt750lem  34795  poimirlem16  37957  itg2addnclem3  37994  fdc  38066  remul02  42837  sn-0tie0  42896  pellqrex  43307  stirlinglem11  46512  fouriersw  46659  zm1nn  47750  evengpoap3  48275