Theorem readdcl 7900

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141  (class class class)co 5853  ℝcr 7773   + caddc 7777

This theorem was proved from axioms:  ax-addrcl 7871

This theorem is referenced by:  0re  7920  readdcli  7933  readdcld  7949  axltadd  7989  peano2re  8055  cnegexlem3  8096  cnegex  8097  resubcl  8183  ltleadd  8365  ltaddsublt  8490  recexap  8571  recreclt  8816  cju  8877  nnge1  8901  addltmul  9114  avglt1  9116  avglt2  9117  avgle1  9118  avgle2  9119  nzadd  9264  irradd  9605  rpaddcl  9634  xaddnemnf  9814  xaddnepnf  9815  xnegdi  9825  xaddass  9826  xltadd1  9833  iooshf  9909  ge0addcl  9938  icoshft  9947  icoshftf1o  9948  iccshftr  9951  difelfznle  10091  elfzodifsumelfzo  10157  subfzo0  10198  serfre  10431  ser3mono  10434  ser3ge0  10473  bernneq  10596  faclbnd6  10678  readd  10833  imadd  10841  elicc4abs  11058  caubnd2  11081  maxabsle  11168  maxabslemval  11172  maxcl  11174  mulcn2  11275  climserle  11308  fsumrecl  11364  mertenslem2  11499  ege2le3  11634  eftlub  11653  efgt1  11660  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem16  12233  xmeter  13230  bl2ioo  13336  ioo2bl  13337  ioo2blex  13338  blssioo  13339  tangtx  13553  relogmul  13584