Theorem readdcli 11334

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

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209   + caddc 11213

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11271

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  resubcli  11630  eqneg  12047  ledivp1i  12252  ltdivp1i  12253  nnne0  12382  2re  12427  3re  12433  4re  12437  5re  12440  6re  12443  7re  12446  8re  12449  9re  12452  10re  12847  numltc  12855  nn0opthlem2  14423  hashunlei  14580  hashge2el2dif  14635  abs3lemi  15590  ef01bndlem  16364  divalglem6  16580  log2ub  27289  mumullem2  27519  bposlem8  27630  dchrvmasumlem2  27837  ex-fl  31060  norm-ii-i  31751  norm3lem  31763  nmoptrii  32708  bdophsi  32710  unierri  32718  staddi  32860  stadd3i  32862  dp2ltc  33506  dpmul4  33533  ballotlem2  35174  hgt750lem  35333  poimirlem16  38694  itg2addnclem3  38731  fdc  38819  remul02  43596  sn-0tie0  43655  pellqrex  44026  stirlinglem11  47233  fouriersw  47380  goldratmolem4  48074  zm1nn  48511  evengpoap3  49036