Theorem readdcli 10921

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801   + caddc 10805

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

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

This theorem is referenced by:  resubcli  11213  eqneg  11625  ledivp1i  11830  ltdivp1i  11831  nnne0  11937  2re  11977  3re  11983  4re  11987  5re  11990  6re  11993  7re  11996  8re  11999  9re  12002  10re  12385  numltc  12392  nn0opthlem2  13911  hashunlei  14068  hashge2el2dif  14122  abs3lemi  15050  ef01bndlem  15821  divalglem6  16035  log2ub  26004  mumullem2  26234  bposlem8  26344  dchrvmasumlem2  26551  ex-fl  28712  norm-ii-i  29400  norm3lem  29412  nmoptrii  30357  bdophsi  30359  unierri  30367  staddi  30509  stadd3i  30511  dp2ltc  31063  dpmul4  31090  ballotlem2  32355  hgt750lem  32531  poimirlem16  35720  itg2addnclem3  35757  fdc  35830  remul02  40309  sn-0tie0  40342  pellqrex  40617  stirlinglem11  43515  fouriersw  43662  zm1nn  44682  evengpoap3  45139