Theorem readdcl 8305

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178   + caddc 8182

This proof depends on axioms:  ax-addrcl 8276

This theorem is used by:  0re  8326  readdcli  8339  readdcld  8355  axltadd  8395  peano2re  8462  cnegexlem3  8503  cnegex  8504  resubcl  8590  ltleadd  8774  ltaddsublt  8900  recexap  8982  recreclt  9231  cju  9292  nnge1  9328  addltmul  9544  avglt1  9546  avglt2  9547  avgle1  9548  avgle2  9549  nzadd  9699  irradd  10048  rpaddcl  10080  xaddnemnf  10261  xaddnepnf  10262  xnegdi  10272  xaddass  10273  xltadd1  10280  iooshf  10356  ge0addcl  10385  icoshft  10394  icoshftf1o  10395  iccshftr  10398  difelfznle  10544  elfzodifsumelfzo  10621  subfzo0  10663  serfre  10923  ser3mono  10926  ser3ge0  10975  bernneq  11100  faclbnd6  11184  ccatsymb  11372  swrdswrdlem  11478  swrdccatin2  11503  readd  11636  imadd  11644  elicc4abs  11862  caubnd2  11885  maxabsle  11972  maxabslemval  11976  maxcl  11978  mulcn2  12080  climserle  12113  fsumrecl  12170  mertenslem2  12305  ege2le3  12440  eftlub  12459  efgt1  12466  pythagtriplem12  13056  pythagtriplem14  13058  pythagtriplem16  13060  xmeter  15539  bl2ioo  15653  ioo2bl  15654  ioo2blex  15655  blssioo  15656  tangtx  15942  relogmul  15974  logfac  16001