Theorem readdcl 7770

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  (class class class)co 5782  ℝcr 7643   + caddc 7647

This theorem was proved from axioms:  ax-addrcl 7741

This theorem is referenced by:  0re  7790  readdcli  7803  readdcld  7819  axltadd  7858  peano2re  7922  cnegexlem3  7963  cnegex  7964  resubcl  8050  ltleadd  8232  ltaddsublt  8357  recexap  8438  recreclt  8682  cju  8743  nnge1  8767  addltmul  8980  avglt1  8982  avglt2  8983  avgle1  8984  avgle2  8985  nzadd  9130  irradd  9465  rpaddcl  9494  xaddnemnf  9670  xaddnepnf  9671  xnegdi  9681  xaddass  9682  xltadd1  9689  iooshf  9765  ge0addcl  9794  icoshft  9803  icoshftf1o  9804  iccshftr  9807  difelfznle  9943  elfzodifsumelfzo  10009  subfzo0  10050  serfre  10279  ser3mono  10282  ser3ge0  10321  bernneq  10443  faclbnd6  10522  readd  10673  imadd  10681  elicc4abs  10898  caubnd2  10921  maxabsle  11008  maxabslemval  11012  maxcl  11014  mulcn2  11113  climserle  11146  fsumrecl  11202  mertenslem2  11337  ege2le3  11414  eftlub  11433  efgt1  11440  xmeter  12644  bl2ioo  12750  ioo2bl  12751  ioo2blex  12752  blssioo  12753  tangtx  12967  relogmul  12998