Theorem readdcli 11301

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

Syntax hints:   ∈ wcel 2103  (class class class)co 7445  ℝcr 11179   + caddc 11183

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

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

This theorem is referenced by:  resubcli  11594  eqneg  12010  ledivp1i  12216  ltdivp1i  12217  nnne0  12323  2re  12363  3re  12369  4re  12373  5re  12376  6re  12379  7re  12382  8re  12385  9re  12388  10re  12773  numltc  12780  nn0opthlem2  14314  hashunlei  14470  hashge2el2dif  14525  abs3lemi  15455  ef01bndlem  16226  divalglem6  16440  log2ub  27001  mumullem2  27232  bposlem8  27344  dchrvmasumlem2  27551  ex-fl  30470  norm-ii-i  31160  norm3lem  31172  nmoptrii  32117  bdophsi  32119  unierri  32127  staddi  32269  stadd3i  32271  dp2ltc  32843  dpmul4  32870  ballotlem2  34445  hgt750lem  34620  poimirlem16  37544  itg2addnclem3  37581  fdc  37653  remul02  42314  sn-0tie0  42348  pellqrex  42772  stirlinglem11  45939  fouriersw  46086  zm1nn  47149  evengpoap3  47605