Theorem readdcli 11147

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

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025   + caddc 11029

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

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

This theorem is referenced by:  resubcli  11443  eqneg  11861  ledivp1i  12067  ltdivp1i  12068  nnne0  12179  2re  12219  3re  12225  4re  12229  5re  12232  6re  12235  7re  12238  8re  12241  9re  12244  10re  12626  numltc  12633  nn0opthlem2  14192  hashunlei  14348  hashge2el2dif  14403  abs3lemi  15334  ef01bndlem  16109  divalglem6  16325  log2ub  26915  mumullem2  27146  bposlem8  27258  dchrvmasumlem2  27465  ex-fl  30522  norm-ii-i  31212  norm3lem  31224  nmoptrii  32169  bdophsi  32171  unierri  32179  staddi  32321  stadd3i  32323  dp2ltc  32968  dpmul4  32995  ballotlem2  34646  hgt750lem  34808  poimirlem16  37837  itg2addnclem3  37874  fdc  37946  remul02  42670  sn-0tie0  42716  pellqrex  43131  stirlinglem11  46338  fouriersw  46485  zm1nn  47558  evengpoap3  48055