Theorem readdcli 10990

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℝcr 10870   + caddc 10874

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

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

This theorem is referenced by:  resubcli  11283  eqneg  11695  ledivp1i  11900  ltdivp1i  11901  nnne0  12007  2re  12047  3re  12053  4re  12057  5re  12060  6re  12063  7re  12066  8re  12069  9re  12072  10re  12456  numltc  12463  nn0opthlem2  13983  hashunlei  14140  hashge2el2dif  14194  abs3lemi  15122  ef01bndlem  15893  divalglem6  16107  log2ub  26099  mumullem2  26329  bposlem8  26439  dchrvmasumlem2  26646  ex-fl  28811  norm-ii-i  29499  norm3lem  29511  nmoptrii  30456  bdophsi  30458  unierri  30466  staddi  30608  stadd3i  30610  dp2ltc  31161  dpmul4  31188  ballotlem2  32455  hgt750lem  32631  poimirlem16  35793  itg2addnclem3  35830  fdc  35903  remul02  40388  sn-0tie0  40421  pellqrex  40701  stirlinglem11  43625  fouriersw  43772  zm1nn  44794  evengpoap3  45251