Theorem readdcl 8151

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6013  ℝcr 8024   + caddc 8028

This theorem was proved from axioms:  ax-addrcl 8122

This theorem is referenced by:  0re  8172  readdcli  8185  readdcld  8202  axltadd  8242  peano2re  8308  cnegexlem3  8349  cnegex  8350  resubcl  8436  ltleadd  8619  ltaddsublt  8744  recexap  8826  recreclt  9073  cju  9134  nnge1  9159  addltmul  9374  avglt1  9376  avglt2  9377  avgle1  9378  avgle2  9379  nzadd  9525  irradd  9873  rpaddcl  9905  xaddnemnf  10085  xaddnepnf  10086  xnegdi  10096  xaddass  10097  xltadd1  10104  iooshf  10180  ge0addcl  10209  icoshft  10218  icoshftf1o  10219  iccshftr  10222  difelfznle  10363  elfzodifsumelfzo  10439  subfzo0  10481  serfre  10739  ser3mono  10742  ser3ge0  10791  bernneq  10915  faclbnd6  10999  ccatsymb  11172  swrdswrdlem  11278  swrdccatin2  11303  readd  11423  imadd  11431  elicc4abs  11648  caubnd2  11671  maxabsle  11758  maxabslemval  11762  maxcl  11764  mulcn2  11866  climserle  11899  fsumrecl  11955  mertenslem2  12090  ege2le3  12225  eftlub  12244  efgt1  12251  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem16  12845  xmeter  15153  bl2ioo  15267  ioo2bl  15268  ioo2blex  15269  blssioo  15270  tangtx  15555  relogmul  15586