Theorem readdcl 8022

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167  (class class class)co 5925  ℝcr 7895   + caddc 7899

This theorem was proved from axioms:  ax-addrcl 7993

This theorem is referenced by:  0re  8043  readdcli  8056  readdcld  8073  axltadd  8113  peano2re  8179  cnegexlem3  8220  cnegex  8221  resubcl  8307  ltleadd  8490  ltaddsublt  8615  recexap  8697  recreclt  8944  cju  9005  nnge1  9030  addltmul  9245  avglt1  9247  avglt2  9248  avgle1  9249  avgle2  9250  nzadd  9395  irradd  9737  rpaddcl  9769  xaddnemnf  9949  xaddnepnf  9950  xnegdi  9960  xaddass  9961  xltadd1  9968  iooshf  10044  ge0addcl  10073  icoshft  10082  icoshftf1o  10083  iccshftr  10086  difelfznle  10227  elfzodifsumelfzo  10294  subfzo0  10335  serfre  10593  ser3mono  10596  ser3ge0  10645  bernneq  10769  faclbnd6  10853  readd  11051  imadd  11059  elicc4abs  11276  caubnd2  11299  maxabsle  11386  maxabslemval  11390  maxcl  11392  mulcn2  11494  climserle  11527  fsumrecl  11583  mertenslem2  11718  ege2le3  11853  eftlub  11872  efgt1  11879  pythagtriplem12  12469  pythagtriplem14  12471  pythagtriplem16  12473  xmeter  14756  bl2ioo  14870  ioo2bl  14871  ioo2blex  14872  blssioo  14873  tangtx  15158  relogmul  15189