Theorem readdcl 7936

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5874  ℝcr 7809   + caddc 7813

This theorem was proved from axioms:  ax-addrcl 7907

This theorem is referenced by:  0re  7956  readdcli  7969  readdcld  7986  axltadd  8026  peano2re  8092  cnegexlem3  8133  cnegex  8134  resubcl  8220  ltleadd  8402  ltaddsublt  8527  recexap  8609  recreclt  8856  cju  8917  nnge1  8941  addltmul  9154  avglt1  9156  avglt2  9157  avgle1  9158  avgle2  9159  nzadd  9304  irradd  9645  rpaddcl  9676  xaddnemnf  9856  xaddnepnf  9857  xnegdi  9867  xaddass  9868  xltadd1  9875  iooshf  9951  ge0addcl  9980  icoshft  9989  icoshftf1o  9990  iccshftr  9993  difelfznle  10134  elfzodifsumelfzo  10200  subfzo0  10241  serfre  10474  ser3mono  10477  ser3ge0  10516  bernneq  10640  faclbnd6  10723  readd  10877  imadd  10885  elicc4abs  11102  caubnd2  11125  maxabsle  11212  maxabslemval  11216  maxcl  11218  mulcn2  11319  climserle  11352  fsumrecl  11408  mertenslem2  11543  ege2le3  11678  eftlub  11697  efgt1  11704  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  xmeter  13906  bl2ioo  14012  ioo2bl  14013  ioo2blex  14014  blssioo  14015  tangtx  14229  relogmul  14260