Theorem readdcli 11324

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199   + caddc 11203

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 11261

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  resubcli  11620  eqneg  12037  ledivp1i  12242  ltdivp1i  12243  nnne0  12372  2re  12417  3re  12423  4re  12427  5re  12430  6re  12433  7re  12436  8re  12439  9re  12442  10re  12837  numltc  12845  nn0opthlem2  14413  hashunlei  14570  hashge2el2dif  14625  abs3lemi  15578  ef01bndlem  16352  divalglem6  16568  log2ub  27277  mumullem2  27507  bposlem8  27618  dchrvmasumlem2  27825  ex-fl  31048  norm-ii-i  31739  norm3lem  31751  nmoptrii  32696  bdophsi  32698  unierri  32706  staddi  32848  stadd3i  32850  dp2ltc  33453  dpmul4  33480  ballotlem2  35121  hgt750lem  35280  poimirlem16  38554  itg2addnclem3  38591  fdc  38679  remul02  43456  sn-0tie0  43515  pellqrex  43885  stirlinglem11  47093  fouriersw  47240  goldratmolem4  47934  zm1nn  48371  evengpoap3  48896