Theorem readdcli 11159

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 7368  ℝ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  11455  eqneg  11873  ledivp1i  12079  ltdivp1i  12080  nnne0  12191  2re  12231  3re  12237  4re  12241  5re  12244  6re  12247  7re  12250  8re  12253  9re  12256  10re  12638  numltc  12645  nn0opthlem2  14204  hashunlei  14360  hashge2el2dif  14415  abs3lemi  15346  ef01bndlem  16121  divalglem6  16337  log2ub  26930  mumullem2  27161  bposlem8  27273  dchrvmasumlem2  27480  ex-fl  30538  norm-ii-i  31229  norm3lem  31241  nmoptrii  32186  bdophsi  32188  unierri  32196  staddi  32338  stadd3i  32340  dp2ltc  32983  dpmul4  33010  ballotlem2  34671  hgt750lem  34833  poimirlem16  37891  itg2addnclem3  37928  fdc  38000  remul02  42779  sn-0tie0  42825  pellqrex  43240  stirlinglem11  46446  fouriersw  46593  zm1nn  47666  evengpoap3  48163