Theorem readdcli 10645

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525   + caddc 10529

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

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  resubcli  10937  eqneg  11349  ledivp1i  11554  ltdivp1i  11555  nnne0  11659  2re  11699  3re  11705  4re  11709  5re  11712  6re  11715  7re  11718  8re  11721  9re  11724  10re  12105  numltc  12112  nn0opthlem2  13625  hashunlei  13782  hashge2el2dif  13834  abs3lemi  14762  ef01bndlem  15529  divalglem6  15739  log2ub  25535  mumullem2  25765  bposlem8  25875  dchrvmasumlem2  26082  ex-fl  28232  norm-ii-i  28920  norm3lem  28932  nmoptrii  29877  bdophsi  29879  unierri  29887  staddi  30029  stadd3i  30031  dp2ltc  30589  dpmul4  30616  ballotlem2  31856  hgt750lem  32032  poimirlem16  35073  itg2addnclem3  35110  fdc  35183  remul02  39543  sn-0tie0  39576  pellqrex  39820  stirlinglem11  42726  fouriersw  42873  zm1nn  43859  evengpoap3  44317