Theorem readdcl 8258

Description: Alias for ax-addrcl 8229, for naming consistency with readdcli 8292. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
readdcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 8229	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6052  ℝcr 8131   + caddc 8135

This theorem was proved from axioms:  ax-addrcl 8229

This theorem is referenced by:  0re  8279  readdcli  8292  readdcld  8308  axltadd  8348  peano2re  8414  cnegexlem3  8455  cnegex  8456  resubcl  8542  ltleadd  8725  ltaddsublt  8850  recexap  8932  recreclt  9179  cju  9240  nnge1  9265  addltmul  9480  avglt1  9482  avglt2  9483  avgle1  9484  avgle2  9485  nzadd  9635  irradd  9984  rpaddcl  10016  xaddnemnf  10196  xaddnepnf  10197  xnegdi  10207  xaddass  10208  xltadd1  10215  iooshf  10291  ge0addcl  10320  icoshft  10329  icoshftf1o  10330  iccshftr  10333  difelfznle  10476  elfzodifsumelfzo  10553  subfzo0  10595  serfre  10853  ser3mono  10856  ser3ge0  10905  bernneq  11030  faclbnd6  11114  ccatsymb  11298  swrdswrdlem  11404  swrdccatin2  11429  readd  11562  imadd  11570  elicc4abs  11787  caubnd2  11810  maxabsle  11897  maxabslemval  11901  maxcl  11903  mulcn2  12005  climserle  12038  fsumrecl  12095  mertenslem2  12230  ege2le3  12365  eftlub  12384  efgt1  12391  pythagtriplem12  12981  pythagtriplem14  12983  pythagtriplem16  12985  xmeter  15350  bl2ioo  15464  ioo2bl  15465  ioo2blex  15466  blssioo  15467  tangtx  15752  relogmul  15783