Theorem readdcli 11195

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7389  ℝcr 11073   + caddc 11077

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

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

This theorem is referenced by:  resubcli  11490  eqneg  11908  ledivp1i  12114  ltdivp1i  12115  nnne0  12221  2re  12261  3re  12267  4re  12271  5re  12274  6re  12277  7re  12280  8re  12283  9re  12286  10re  12674  numltc  12681  nn0opthlem2  14240  hashunlei  14396  hashge2el2dif  14451  abs3lemi  15383  ef01bndlem  16158  divalglem6  16374  log2ub  26865  mumullem2  27096  bposlem8  27208  dchrvmasumlem2  27415  ex-fl  30382  norm-ii-i  31072  norm3lem  31084  nmoptrii  32029  bdophsi  32031  unierri  32039  staddi  32181  stadd3i  32183  dp2ltc  32813  dpmul4  32840  ballotlem2  34486  hgt750lem  34648  poimirlem16  37625  itg2addnclem3  37662  fdc  37734  remul02  42388  sn-0tie0  42434  pellqrex  42860  stirlinglem11  46075  fouriersw  46222  zm1nn  47293  evengpoap3  47790