Theorem readdcl 8249

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2203  (class class class)co 6049  ℝcr 8122   + caddc 8126

This theorem was proved from axioms:  ax-addrcl 8220

This theorem is referenced by:  0re  8270  readdcli  8283  readdcld  8299  axltadd  8339  peano2re  8405  cnegexlem3  8446  cnegex  8447  resubcl  8533  ltleadd  8716  ltaddsublt  8841  recexap  8923  recreclt  9170  cju  9231  nnge1  9256  addltmul  9471  avglt1  9473  avglt2  9474  avgle1  9475  avgle2  9476  nzadd  9626  irradd  9974  rpaddcl  10006  xaddnemnf  10186  xaddnepnf  10187  xnegdi  10197  xaddass  10198  xltadd1  10205  iooshf  10281  ge0addcl  10310  icoshft  10319  icoshftf1o  10320  iccshftr  10323  difelfznle  10465  elfzodifsumelfzo  10542  subfzo0  10584  serfre  10842  ser3mono  10845  ser3ge0  10894  bernneq  11018  faclbnd6  11102  ccatsymb  11283  swrdswrdlem  11389  swrdccatin2  11414  readd  11547  imadd  11555  elicc4abs  11772  caubnd2  11795  maxabsle  11882  maxabslemval  11886  maxcl  11888  mulcn2  11990  climserle  12023  fsumrecl  12080  mertenslem2  12215  ege2le3  12350  eftlub  12369  efgt1  12376  pythagtriplem12  12966  pythagtriplem14  12968  pythagtriplem16  12970  xmeter  15288  bl2ioo  15402  ioo2bl  15403  ioo2blex  15404  blssioo  15405  tangtx  15690  relogmul  15721