Theorem readdcli 11127

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005   + caddc 11009

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

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

This theorem is referenced by:  resubcli  11423  eqneg  11841  ledivp1i  12047  ltdivp1i  12048  nnne0  12159  2re  12199  3re  12205  4re  12209  5re  12212  6re  12215  7re  12218  8re  12221  9re  12224  10re  12607  numltc  12614  nn0opthlem2  14176  hashunlei  14332  hashge2el2dif  14387  abs3lemi  15318  ef01bndlem  16093  divalglem6  16309  log2ub  26886  mumullem2  27117  bposlem8  27229  dchrvmasumlem2  27436  ex-fl  30427  norm-ii-i  31117  norm3lem  31129  nmoptrii  32074  bdophsi  32076  unierri  32084  staddi  32226  stadd3i  32228  dp2ltc  32867  dpmul4  32894  ballotlem2  34502  hgt750lem  34664  poimirlem16  37686  itg2addnclem3  37723  fdc  37795  remul02  42508  sn-0tie0  42554  pellqrex  42982  stirlinglem11  46192  fouriersw  46339  zm1nn  47412  evengpoap3  47909