Theorem readdcli 11151

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

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028   + caddc 11032

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

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

This theorem is referenced by:  resubcli  11447  eqneg  11866  ledivp1i  12072  ltdivp1i  12073  nnne0  12202  2re  12246  3re  12252  4re  12256  5re  12259  6re  12262  7re  12265  8re  12268  9re  12271  10re  12654  numltc  12661  nn0opthlem2  14222  hashunlei  14378  hashge2el2dif  14433  abs3lemi  15364  ef01bndlem  16142  divalglem6  16358  log2ub  26931  mumullem2  27161  bposlem8  27272  dchrvmasumlem2  27479  ex-fl  30535  norm-ii-i  31226  norm3lem  31238  nmoptrii  32183  bdophsi  32185  unierri  32193  staddi  32335  stadd3i  32337  dp2ltc  32965  dpmul4  32992  ballotlem2  34673  hgt750lem  34835  poimirlem16  38003  itg2addnclem3  38040  fdc  38112  remul02  42882  sn-0tie0  42941  pellqrex  43324  stirlinglem11  46527  fouriersw  46674  zm1nn  47765  evengpoap3  48290