Theorem readdcli 11233

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

Syntax hints:   ∈ wcel 2104  (class class class)co 7411  ℝcr 11111   + caddc 11115

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

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

This theorem is referenced by:  resubcli  11526  eqneg  11938  ledivp1i  12143  ltdivp1i  12144  nnne0  12250  2re  12290  3re  12296  4re  12300  5re  12303  6re  12306  7re  12309  8re  12312  9re  12315  10re  12700  numltc  12707  nn0opthlem2  14233  hashunlei  14389  hashge2el2dif  14445  abs3lemi  15361  ef01bndlem  16131  divalglem6  16345  log2ub  26690  mumullem2  26920  bposlem8  27030  dchrvmasumlem2  27237  ex-fl  29967  norm-ii-i  30657  norm3lem  30669  nmoptrii  31614  bdophsi  31616  unierri  31624  staddi  31766  stadd3i  31768  dp2ltc  32320  dpmul4  32347  ballotlem2  33785  hgt750lem  33961  poimirlem16  36807  itg2addnclem3  36844  fdc  36916  remul02  41580  sn-0tie0  41614  pellqrex  41919  stirlinglem11  45098  fouriersw  45245  zm1nn  46308  evengpoap3  46765