Theorem readdcli 11224

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

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℝcr 11099   + caddc 11103

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  resubcli  11520  eqneg  11935  ledivp1i  12140  ltdivp1i  12141  nnne0  12270  2re  12315  3re  12321  4re  12325  5re  12328  6re  12331  7re  12334  8re  12337  9re  12340  10re  12734  numltc  12742  nn0opthlem2  14305  hashunlei  14462  hashge2el2dif  14517  abs3lemi  15462  ef01bndlem  16240  divalglem6  16456  log2ub  27080  mumullem2  27310  bposlem8  27421  dchrvmasumlem2  27628  ex-fl  30739  norm-ii-i  31430  norm3lem  31442  nmoptrii  32387  bdophsi  32389  unierri  32397  staddi  32539  stadd3i  32541  dp2ltc  33147  dpmul4  33174  ballotlem2  34824  hgt750lem  34983  poimirlem16  38175  itg2addnclem3  38212  fdc  38284  remul02  43056  sn-0tie0  43115  pellqrex  43498  stirlinglem11  46690  fouriersw  46837  zm1nn  47928  evengpoap3  48453