Theorem readdcl 8005

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5922  ℝcr 7878   + caddc 7882

This theorem was proved from axioms:  ax-addrcl 7976

This theorem is referenced by:  0re  8026  readdcli  8039  readdcld  8056  axltadd  8096  peano2re  8162  cnegexlem3  8203  cnegex  8204  resubcl  8290  ltleadd  8473  ltaddsublt  8598  recexap  8680  recreclt  8927  cju  8988  nnge1  9013  addltmul  9228  avglt1  9230  avglt2  9231  avgle1  9232  avgle2  9233  nzadd  9378  irradd  9720  rpaddcl  9752  xaddnemnf  9932  xaddnepnf  9933  xnegdi  9943  xaddass  9944  xltadd1  9951  iooshf  10027  ge0addcl  10056  icoshft  10065  icoshftf1o  10066  iccshftr  10069  difelfznle  10210  elfzodifsumelfzo  10277  subfzo0  10318  serfre  10576  ser3mono  10579  ser3ge0  10628  bernneq  10752  faclbnd6  10836  readd  11034  imadd  11042  elicc4abs  11259  caubnd2  11282  maxabsle  11369  maxabslemval  11373  maxcl  11375  mulcn2  11477  climserle  11510  fsumrecl  11566  mertenslem2  11701  ege2le3  11836  eftlub  11855  efgt1  11862  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  xmeter  14672  bl2ioo  14786  ioo2bl  14787  ioo2blex  14788  blssioo  14789  tangtx  15074  relogmul  15105