Theorem readdcl 8312

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

Assertion

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

Proof of Theorem readdcl

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  (class class class)co 6088  ℝcr 8185   + caddc 8189

This proof depends on axioms:  ax-addrcl 8283

This theorem is used by:  0re  8333  readdcli  8346  readdcld  8362  axltadd  8402  peano2re  8470  cnegexlem3  8511  cnegex  8512  resubcl  8598  ltleadd  8782  ltaddsublt  8908  recexap  8990  recreclt  9239  cju  9300  nnge1  9337  addltmul  9554  avglt1  9556  avglt2  9557  avgle1  9558  avgle2  9559  nzadd  9709  irradd  10063  rpaddcl  10096  xaddnemnf  10277  xaddnepnf  10278  xnegdi  10288  xaddass  10289  xltadd1  10296  iooshf  10372  ge0addcl  10401  icoshft  10410  icoshftf1o  10411  iccshftr  10414  difelfznle  10560  elfzodifsumelfzo  10637  subfzo0  10679  serfre  10943  ser3mono  10946  ser3ge0  10995  bernneq  11120  faclbnd6  11205  ccatsymb  11393  swrdswrdlem  11499  swrdccatin2  11524  readd  11657  imadd  11665  elicc4abs  11884  caubnd2  11907  maxabsle  11994  maxabslemval  11998  maxcl  12000  mulcn2  12104  climserle  12137  fsumrecl  12194  mertenslem2  12329  ege2le3  12464  eftlub  12483  efgt1  12490  pythagtriplem12  13084  pythagtriplem14  13086  pythagtriplem16  13088  xmeter  15674  bl2ioo  15788  ioo2bl  15789  ioo2blex  15790  blssioo  15791  tangtx  16077  relogmul  16111  logfac  16138  ppiqub  16305  bposlem5  16327  bposlem6  16328  bposlem9  16331