Theorem readdcl 8299

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6079  ℝcr 8172   + caddc 8176

This theorem was proved from axioms:  ax-addrcl 8270

This theorem is referenced by:  0re  8320  readdcli  8333  readdcld  8349  axltadd  8389  peano2re  8456  cnegexlem3  8497  cnegex  8498  resubcl  8584  ltleadd  8768  ltaddsublt  8893  recexap  8975  recreclt  9224  cju  9285  nnge1  9310  addltmul  9525  avglt1  9527  avglt2  9528  avgle1  9529  avgle2  9530  nzadd  9680  irradd  10029  rpaddcl  10061  xaddnemnf  10242  xaddnepnf  10243  xnegdi  10253  xaddass  10254  xltadd1  10261  iooshf  10337  ge0addcl  10366  icoshft  10375  icoshftf1o  10376  iccshftr  10379  difelfznle  10525  elfzodifsumelfzo  10602  subfzo0  10644  serfre  10904  ser3mono  10907  ser3ge0  10956  bernneq  11081  faclbnd6  11165  ccatsymb  11353  swrdswrdlem  11459  swrdccatin2  11484  readd  11617  imadd  11625  elicc4abs  11843  caubnd2  11866  maxabsle  11953  maxabslemval  11957  maxcl  11959  mulcn2  12061  climserle  12094  fsumrecl  12151  mertenslem2  12286  ege2le3  12421  eftlub  12440  efgt1  12447  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem16  13041  xmeter  15520  bl2ioo  15634  ioo2bl  15635  ioo2blex  15636  blssioo  15637  tangtx  15922  relogmul  15953  logfac  15978