Theorem readdcli 11277

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155   + caddc 11159

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

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

This theorem is referenced by:  resubcli  11572  eqneg  11988  ledivp1i  12194  ltdivp1i  12195  nnne0  12301  2re  12341  3re  12347  4re  12351  5re  12354  6re  12357  7re  12360  8re  12363  9re  12366  10re  12754  numltc  12761  nn0opthlem2  14309  hashunlei  14465  hashge2el2dif  14520  abs3lemi  15450  ef01bndlem  16221  divalglem6  16436  log2ub  26993  mumullem2  27224  bposlem8  27336  dchrvmasumlem2  27543  ex-fl  30467  norm-ii-i  31157  norm3lem  31169  nmoptrii  32114  bdophsi  32116  unierri  32124  staddi  32266  stadd3i  32268  dp2ltc  32870  dpmul4  32897  ballotlem2  34492  hgt750lem  34667  poimirlem16  37644  itg2addnclem3  37681  fdc  37753  remul02  42440  sn-0tie0  42474  pellqrex  42895  stirlinglem11  46104  fouriersw  46251  zm1nn  47319  evengpoap3  47791