Theorem readdcli 11251

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

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℝcr 11129   + caddc 11133

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

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

This theorem is referenced by:  resubcli  11544  eqneg  11956  ledivp1i  12161  ltdivp1i  12162  nnne0  12268  2re  12308  3re  12314  4re  12318  5re  12321  6re  12324  7re  12327  8re  12330  9re  12333  10re  12718  numltc  12725  nn0opthlem2  14252  hashunlei  14408  hashge2el2dif  14465  abs3lemi  15381  ef01bndlem  16152  divalglem6  16366  log2ub  26868  mumullem2  27099  bposlem8  27211  dchrvmasumlem2  27418  ex-fl  30244  norm-ii-i  30934  norm3lem  30946  nmoptrii  31891  bdophsi  31893  unierri  31901  staddi  32043  stadd3i  32045  dp2ltc  32592  dpmul4  32619  ballotlem2  34044  hgt750lem  34219  poimirlem16  37044  itg2addnclem3  37081  fdc  37153  remul02  41882  sn-0tie0  41916  pellqrex  42221  stirlinglem11  45395  fouriersw  45542  zm1nn  46605  evengpoap3  47062