Theorem readdcli 11165

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043   + caddc 11047

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

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

This theorem is referenced by:  resubcli  11460  eqneg  11878  ledivp1i  12084  ltdivp1i  12085  nnne0  12196  2re  12236  3re  12242  4re  12246  5re  12249  6re  12252  7re  12255  8re  12258  9re  12261  10re  12644  numltc  12651  nn0opthlem2  14210  hashunlei  14366  hashge2el2dif  14421  abs3lemi  15353  ef01bndlem  16128  divalglem6  16344  log2ub  26892  mumullem2  27123  bposlem8  27235  dchrvmasumlem2  27442  ex-fl  30426  norm-ii-i  31116  norm3lem  31128  nmoptrii  32073  bdophsi  32075  unierri  32083  staddi  32225  stadd3i  32227  dp2ltc  32857  dpmul4  32884  ballotlem2  34473  hgt750lem  34635  poimirlem16  37623  itg2addnclem3  37660  fdc  37732  remul02  42386  sn-0tie0  42432  pellqrex  42860  stirlinglem11  46075  fouriersw  46222  zm1nn  47296  evengpoap3  47793