Theorem readdcl 8141

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6010  ℝcr 8014   + caddc 8018

This theorem was proved from axioms:  ax-addrcl 8112

This theorem is referenced by:  0re  8162  readdcli  8175  readdcld  8192  axltadd  8232  peano2re  8298  cnegexlem3  8339  cnegex  8340  resubcl  8426  ltleadd  8609  ltaddsublt  8734  recexap  8816  recreclt  9063  cju  9124  nnge1  9149  addltmul  9364  avglt1  9366  avglt2  9367  avgle1  9368  avgle2  9369  nzadd  9515  irradd  9858  rpaddcl  9890  xaddnemnf  10070  xaddnepnf  10071  xnegdi  10081  xaddass  10082  xltadd1  10089  iooshf  10165  ge0addcl  10194  icoshft  10203  icoshftf1o  10204  iccshftr  10207  difelfznle  10348  elfzodifsumelfzo  10424  subfzo0  10465  serfre  10723  ser3mono  10726  ser3ge0  10775  bernneq  10899  faclbnd6  10983  ccatsymb  11155  swrdswrdlem  11257  swrdccatin2  11282  readd  11401  imadd  11409  elicc4abs  11626  caubnd2  11649  maxabsle  11736  maxabslemval  11740  maxcl  11742  mulcn2  11844  climserle  11877  fsumrecl  11933  mertenslem2  12068  ege2le3  12203  eftlub  12222  efgt1  12229  pythagtriplem12  12819  pythagtriplem14  12821  pythagtriplem16  12823  xmeter  15131  bl2ioo  15245  ioo2bl  15246  ioo2blex  15247  blssioo  15248  tangtx  15533  relogmul  15564