Theorem readdcli 11274

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

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℝcr 11152   + caddc 11156

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

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

This theorem is referenced by:  resubcli  11569  eqneg  11985  ledivp1i  12191  ltdivp1i  12192  nnne0  12298  2re  12338  3re  12344  4re  12348  5re  12351  6re  12354  7re  12357  8re  12360  9re  12363  10re  12750  numltc  12757  nn0opthlem2  14305  hashunlei  14461  hashge2el2dif  14516  abs3lemi  15446  ef01bndlem  16217  divalglem6  16432  log2ub  27007  mumullem2  27238  bposlem8  27350  dchrvmasumlem2  27557  ex-fl  30476  norm-ii-i  31166  norm3lem  31178  nmoptrii  32123  bdophsi  32125  unierri  32133  staddi  32275  stadd3i  32277  dp2ltc  32854  dpmul4  32881  ballotlem2  34470  hgt750lem  34645  poimirlem16  37623  itg2addnclem3  37660  fdc  37732  remul02  42412  sn-0tie0  42446  pellqrex  42867  stirlinglem11  46040  fouriersw  46187  zm1nn  47252  evengpoap3  47724