Theorem readdcli 11225

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℝcr 11105   + caddc 11109

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

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

This theorem is referenced by:  resubcli  11518  eqneg  11930  ledivp1i  12135  ltdivp1i  12136  nnne0  12242  2re  12282  3re  12288  4re  12292  5re  12295  6re  12298  7re  12301  8re  12304  9re  12307  10re  12692  numltc  12699  nn0opthlem2  14225  hashunlei  14381  hashge2el2dif  14437  abs3lemi  15353  ef01bndlem  16123  divalglem6  16337  log2ub  26443  mumullem2  26673  bposlem8  26783  dchrvmasumlem2  26990  ex-fl  29689  norm-ii-i  30377  norm3lem  30389  nmoptrii  31334  bdophsi  31336  unierri  31344  staddi  31486  stadd3i  31488  dp2ltc  32040  dpmul4  32067  ballotlem2  33475  hgt750lem  33651  poimirlem16  36492  itg2addnclem3  36529  fdc  36601  remul02  41274  sn-0tie0  41308  pellqrex  41602  stirlinglem11  44786  fouriersw  44933  zm1nn  45996  evengpoap3  46453