Theorem readdcli 11255

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

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133   + caddc 11137

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

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

This theorem is referenced by:  resubcli  11550  eqneg  11966  ledivp1i  12172  ltdivp1i  12173  nnne0  12279  2re  12319  3re  12325  4re  12329  5re  12332  6re  12335  7re  12338  8re  12341  9re  12344  10re  12732  numltc  12739  nn0opthlem2  14292  hashunlei  14448  hashge2el2dif  14503  abs3lemi  15434  ef01bndlem  16207  divalglem6  16422  log2ub  26916  mumullem2  27147  bposlem8  27259  dchrvmasumlem2  27466  ex-fl  30433  norm-ii-i  31123  norm3lem  31135  nmoptrii  32080  bdophsi  32082  unierri  32090  staddi  32232  stadd3i  32234  dp2ltc  32866  dpmul4  32893  ballotlem2  34526  hgt750lem  34688  poimirlem16  37665  itg2addnclem3  37702  fdc  37774  remul02  42423  sn-0tie0  42457  pellqrex  42877  stirlinglem11  46093  fouriersw  46240  zm1nn  47311  evengpoap3  47793