Theorem readdcl 8269

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142   + caddc 8146

This theorem was proved from axioms:  ax-addrcl 8240

This theorem is referenced by:  0re  8290  readdcli  8303  readdcld  8319  axltadd  8359  peano2re  8426  cnegexlem3  8467  cnegex  8468  resubcl  8554  ltleadd  8738  ltaddsublt  8863  recexap  8945  recreclt  9194  cju  9255  nnge1  9280  addltmul  9495  avglt1  9497  avglt2  9498  avgle1  9499  avgle2  9500  nzadd  9650  irradd  9999  rpaddcl  10031  xaddnemnf  10212  xaddnepnf  10213  xnegdi  10223  xaddass  10224  xltadd1  10231  iooshf  10307  ge0addcl  10336  icoshft  10345  icoshftf1o  10346  iccshftr  10349  difelfznle  10494  elfzodifsumelfzo  10571  subfzo0  10613  serfre  10873  ser3mono  10876  ser3ge0  10925  bernneq  11050  faclbnd6  11134  ccatsymb  11318  swrdswrdlem  11424  swrdccatin2  11449  readd  11582  imadd  11590  elicc4abs  11807  caubnd2  11830  maxabsle  11917  maxabslemval  11921  maxcl  11923  mulcn2  12025  climserle  12058  fsumrecl  12115  mertenslem2  12250  ege2le3  12385  eftlub  12404  efgt1  12411  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem16  13005  xmeter  15430  bl2ioo  15544  ioo2bl  15545  ioo2blex  15546  blssioo  15547  tangtx  15832  relogmul  15863