Theorem readdcli 11197

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

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072   + caddc 11076

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

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  resubcli  11493  eqneg  11911  ledivp1i  12117  ltdivp1i  12118  nnne0  12247  2re  12292  3re  12298  4re  12302  5re  12305  6re  12308  7re  12311  8re  12314  9re  12317  10re  12711  numltc  12719  nn0opthlem2  14282  hashunlei  14438  hashge2el2dif  14493  abs3lemi  15438  ef01bndlem  16216  divalglem6  16432  log2ub  27014  mumullem2  27244  bposlem8  27355  dchrvmasumlem2  27562  ex-fl  30649  norm-ii-i  31340  norm3lem  31352  nmoptrii  32297  bdophsi  32299  unierri  32307  staddi  32449  stadd3i  32451  dp2ltc  33064  dpmul4  33091  ballotlem2  34786  hgt750lem  34945  poimirlem16  38135  itg2addnclem3  38172  fdc  38244  remul02  43014  sn-0tie0  43073  pellqrex  43456  stirlinglem11  46658  fouriersw  46805  zm1nn  47896  evengpoap3  48421