Theorem readdcl 8158

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031   + caddc 8035

This theorem was proved from axioms:  ax-addrcl 8129

This theorem is referenced by:  0re  8179  readdcli  8192  readdcld  8209  axltadd  8249  peano2re  8315  cnegexlem3  8356  cnegex  8357  resubcl  8443  ltleadd  8626  ltaddsublt  8751  recexap  8833  recreclt  9080  cju  9141  nnge1  9166  addltmul  9381  avglt1  9383  avglt2  9384  avgle1  9385  avgle2  9386  nzadd  9532  irradd  9880  rpaddcl  9912  xaddnemnf  10092  xaddnepnf  10093  xnegdi  10103  xaddass  10104  xltadd1  10111  iooshf  10187  ge0addcl  10216  icoshft  10225  icoshftf1o  10226  iccshftr  10229  difelfznle  10370  elfzodifsumelfzo  10447  subfzo0  10489  serfre  10747  ser3mono  10750  ser3ge0  10799  bernneq  10923  faclbnd6  11007  ccatsymb  11180  swrdswrdlem  11286  swrdccatin2  11311  readd  11431  imadd  11439  elicc4abs  11656  caubnd2  11679  maxabsle  11766  maxabslemval  11770  maxcl  11772  mulcn2  11874  climserle  11907  fsumrecl  11964  mertenslem2  12099  ege2le3  12234  eftlub  12253  efgt1  12260  pythagtriplem12  12850  pythagtriplem14  12852  pythagtriplem16  12854  xmeter  15163  bl2ioo  15277  ioo2bl  15278  ioo2blex  15279  blssioo  15280  tangtx  15565  relogmul  15596