Theorem readdcl 8000

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5919  ℝcr 7873   + caddc 7877

This theorem was proved from axioms:  ax-addrcl 7971

This theorem is referenced by:  0re  8021  readdcli  8034  readdcld  8051  axltadd  8091  peano2re  8157  cnegexlem3  8198  cnegex  8199  resubcl  8285  ltleadd  8467  ltaddsublt  8592  recexap  8674  recreclt  8921  cju  8982  nnge1  9007  addltmul  9222  avglt1  9224  avglt2  9225  avgle1  9226  avgle2  9227  nzadd  9372  irradd  9714  rpaddcl  9746  xaddnemnf  9926  xaddnepnf  9927  xnegdi  9937  xaddass  9938  xltadd1  9945  iooshf  10021  ge0addcl  10050  icoshft  10059  icoshftf1o  10060  iccshftr  10063  difelfznle  10204  elfzodifsumelfzo  10271  subfzo0  10312  serfre  10558  ser3mono  10561  ser3ge0  10610  bernneq  10734  faclbnd6  10818  readd  11016  imadd  11024  elicc4abs  11241  caubnd2  11264  maxabsle  11351  maxabslemval  11355  maxcl  11357  mulcn2  11458  climserle  11491  fsumrecl  11547  mertenslem2  11682  ege2le3  11817  eftlub  11836  efgt1  11843  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem16  12420  xmeter  14615  bl2ioo  14729  ioo2bl  14730  ioo2blex  14731  blssioo  14732  tangtx  15014  relogmul  15045