Theorem readdcli 11305

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

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183   + caddc 11187

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

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

This theorem is referenced by:  resubcli  11598  eqneg  12014  ledivp1i  12220  ltdivp1i  12221  nnne0  12327  2re  12367  3re  12373  4re  12377  5re  12380  6re  12383  7re  12386  8re  12389  9re  12392  10re  12777  numltc  12784  nn0opthlem2  14318  hashunlei  14474  hashge2el2dif  14529  abs3lemi  15459  ef01bndlem  16232  divalglem6  16446  log2ub  27010  mumullem2  27241  bposlem8  27353  dchrvmasumlem2  27560  ex-fl  30479  norm-ii-i  31169  norm3lem  31181  nmoptrii  32126  bdophsi  32128  unierri  32136  staddi  32278  stadd3i  32280  dp2ltc  32851  dpmul4  32878  ballotlem2  34453  hgt750lem  34628  poimirlem16  37596  itg2addnclem3  37633  fdc  37705  remul02  42381  sn-0tie0  42415  pellqrex  42835  stirlinglem11  46005  fouriersw  46152  zm1nn  47217  evengpoap3  47673