Theorem readdcli 10053

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

Syntax hints:   ∈ wcel 1990  (class class class)co 6650  ℝcr 9935   + caddc 9939

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

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  resubcli  10343  eqneg  10745  ledivp1i  10949  ltdivp1i  10950  2re  11090  3re  11094  4re  11097  5re  11099  6re  11101  7re  11103  8re  11105  9re  11107  10reOLD  11109  numltc  11528  nn0opthlem2  13056  hashunlei  13212  hashge2el2dif  13262  abs3lemi  14149  ef01bndlem  14914  divalglem6  15121  log2ub  24676  mumullem2  24906  bposlem8  25016  dchrvmasumlem2  25187  ex-fl  27304  norm-ii-i  27994  norm3lem  28006  nmoptrii  28953  bdophsi  28955  unierri  28963  staddi  29105  stadd3i  29107  dp2ltc  29594  dpmul4  29622  ballotlem2  30550  hgt750lem  30729  poimirlem16  33425  itg2addnclem3  33463  fdc  33541  pellqrex  37443  stirlinglem11  40301  fouriersw  40448  zm1nn  41316  evengpoap3  41687