Theorem readdcli 11154

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031   + caddc 11035

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

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

This theorem is referenced by:  resubcli  11450  eqneg  11869  ledivp1i  12075  ltdivp1i  12076  nnne0  12205  2re  12249  3re  12255  4re  12259  5re  12262  6re  12265  7re  12268  8re  12271  9re  12274  10re  12657  numltc  12664  nn0opthlem2  14225  hashunlei  14381  hashge2el2dif  14436  abs3lemi  15367  ef01bndlem  16145  divalglem6  16361  log2ub  26929  mumullem2  27160  bposlem8  27271  dchrvmasumlem2  27478  ex-fl  30535  norm-ii-i  31226  norm3lem  31238  nmoptrii  32183  bdophsi  32185  unierri  32193  staddi  32335  stadd3i  32337  dp2ltc  32964  dpmul4  32991  ballotlem2  34652  hgt750lem  34814  poimirlem16  37974  itg2addnclem3  38011  fdc  38083  remul02  42854  sn-0tie0  42913  pellqrex  43328  stirlinglem11  46533  fouriersw  46680  zm1nn  47765  evengpoap3  48290