Theorem readdcl 8024

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897   + caddc 7901

This theorem was proved from axioms:  ax-addrcl 7995

This theorem is referenced by:  0re  8045  readdcli  8058  readdcld  8075  axltadd  8115  peano2re  8181  cnegexlem3  8222  cnegex  8223  resubcl  8309  ltleadd  8492  ltaddsublt  8617  recexap  8699  recreclt  8946  cju  9007  nnge1  9032  addltmul  9247  avglt1  9249  avglt2  9250  avgle1  9251  avgle2  9252  nzadd  9397  irradd  9739  rpaddcl  9771  xaddnemnf  9951  xaddnepnf  9952  xnegdi  9962  xaddass  9963  xltadd1  9970  iooshf  10046  ge0addcl  10075  icoshft  10084  icoshftf1o  10085  iccshftr  10088  difelfznle  10229  elfzodifsumelfzo  10296  subfzo0  10337  serfre  10595  ser3mono  10598  ser3ge0  10647  bernneq  10771  faclbnd6  10855  readd  11053  imadd  11061  elicc4abs  11278  caubnd2  11301  maxabsle  11388  maxabslemval  11392  maxcl  11394  mulcn2  11496  climserle  11529  fsumrecl  11585  mertenslem2  11720  ege2le3  11855  eftlub  11874  efgt1  11881  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem16  12475  xmeter  14758  bl2ioo  14872  ioo2bl  14873  ioo2blex  14874  blssioo  14875  tangtx  15160  relogmul  15191