Theorem readdcl 7950

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2158  (class class class)co 5888  ℝcr 7823   + caddc 7827

This theorem was proved from axioms:  ax-addrcl 7921

This theorem is referenced by:  0re  7970  readdcli  7983  readdcld  8000  axltadd  8040  peano2re  8106  cnegexlem3  8147  cnegex  8148  resubcl  8234  ltleadd  8416  ltaddsublt  8541  recexap  8623  recreclt  8870  cju  8931  nnge1  8955  addltmul  9168  avglt1  9170  avglt2  9171  avgle1  9172  avgle2  9173  nzadd  9318  irradd  9659  rpaddcl  9690  xaddnemnf  9870  xaddnepnf  9871  xnegdi  9881  xaddass  9882  xltadd1  9889  iooshf  9965  ge0addcl  9994  icoshft  10003  icoshftf1o  10004  iccshftr  10007  difelfznle  10148  elfzodifsumelfzo  10214  subfzo0  10255  serfre  10488  ser3mono  10491  ser3ge0  10530  bernneq  10654  faclbnd6  10737  readd  10891  imadd  10899  elicc4abs  11116  caubnd2  11139  maxabsle  11226  maxabslemval  11230  maxcl  11232  mulcn2  11333  climserle  11366  fsumrecl  11422  mertenslem2  11557  ege2le3  11692  eftlub  11711  efgt1  11718  pythagtriplem12  12288  pythagtriplem14  12290  pythagtriplem16  12292  xmeter  14207  bl2ioo  14313  ioo2bl  14314  ioo2blex  14315  blssioo  14316  tangtx  14530  relogmul  14561