Theorem readdcl 8163

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2201  (class class class)co 6023  ℝcr 8036   + caddc 8040

This theorem was proved from axioms:  ax-addrcl 8134

This theorem is referenced by:  0re  8184  readdcli  8197  readdcld  8214  axltadd  8254  peano2re  8320  cnegexlem3  8361  cnegex  8362  resubcl  8448  ltleadd  8631  ltaddsublt  8756  recexap  8838  recreclt  9085  cju  9146  nnge1  9171  addltmul  9386  avglt1  9388  avglt2  9389  avgle1  9390  avgle2  9391  nzadd  9537  irradd  9885  rpaddcl  9917  xaddnemnf  10097  xaddnepnf  10098  xnegdi  10108  xaddass  10109  xltadd1  10116  iooshf  10192  ge0addcl  10221  icoshft  10230  icoshftf1o  10231  iccshftr  10234  difelfznle  10375  elfzodifsumelfzo  10452  subfzo0  10494  serfre  10752  ser3mono  10755  ser3ge0  10804  bernneq  10928  faclbnd6  11012  ccatsymb  11188  swrdswrdlem  11294  swrdccatin2  11319  readd  11452  imadd  11460  elicc4abs  11677  caubnd2  11700  maxabsle  11787  maxabslemval  11791  maxcl  11793  mulcn2  11895  climserle  11928  fsumrecl  11985  mertenslem2  12120  ege2le3  12255  eftlub  12274  efgt1  12281  pythagtriplem12  12871  pythagtriplem14  12873  pythagtriplem16  12875  xmeter  15189  bl2ioo  15303  ioo2bl  15304  ioo2blex  15305  blssioo  15306  tangtx  15591  relogmul  15622