Theorem readdcl 8058

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  (class class class)co 5951  ℝcr 7931   + caddc 7935

This theorem was proved from axioms:  ax-addrcl 8029

This theorem is referenced by:  0re  8079  readdcli  8092  readdcld  8109  axltadd  8149  peano2re  8215  cnegexlem3  8256  cnegex  8257  resubcl  8343  ltleadd  8526  ltaddsublt  8651  recexap  8733  recreclt  8980  cju  9041  nnge1  9066  addltmul  9281  avglt1  9283  avglt2  9284  avgle1  9285  avgle2  9286  nzadd  9432  irradd  9774  rpaddcl  9806  xaddnemnf  9986  xaddnepnf  9987  xnegdi  9997  xaddass  9998  xltadd1  10005  iooshf  10081  ge0addcl  10110  icoshft  10119  icoshftf1o  10120  iccshftr  10123  difelfznle  10264  elfzodifsumelfzo  10337  subfzo0  10378  serfre  10636  ser3mono  10639  ser3ge0  10688  bernneq  10812  faclbnd6  10896  ccatsymb  11066  swrdswrdlem  11163  readd  11224  imadd  11232  elicc4abs  11449  caubnd2  11472  maxabsle  11559  maxabslemval  11563  maxcl  11565  mulcn2  11667  climserle  11700  fsumrecl  11756  mertenslem2  11891  ege2le3  12026  eftlub  12045  efgt1  12052  pythagtriplem12  12642  pythagtriplem14  12644  pythagtriplem16  12646  xmeter  14952  bl2ioo  15066  ioo2bl  15067  ioo2blex  15068  blssioo  15069  tangtx  15354  relogmul  15385