Theorem readdcl 8133

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  (class class class)co 6007  ℝcr 8006   + caddc 8010

This theorem was proved from axioms:  ax-addrcl 8104

This theorem is referenced by:  0re  8154  readdcli  8167  readdcld  8184  axltadd  8224  peano2re  8290  cnegexlem3  8331  cnegex  8332  resubcl  8418  ltleadd  8601  ltaddsublt  8726  recexap  8808  recreclt  9055  cju  9116  nnge1  9141  addltmul  9356  avglt1  9358  avglt2  9359  avgle1  9360  avgle2  9361  nzadd  9507  irradd  9849  rpaddcl  9881  xaddnemnf  10061  xaddnepnf  10062  xnegdi  10072  xaddass  10073  xltadd1  10080  iooshf  10156  ge0addcl  10185  icoshft  10194  icoshftf1o  10195  iccshftr  10198  difelfznle  10339  elfzodifsumelfzo  10415  subfzo0  10456  serfre  10714  ser3mono  10717  ser3ge0  10766  bernneq  10890  faclbnd6  10974  ccatsymb  11145  swrdswrdlem  11244  swrdccatin2  11269  readd  11388  imadd  11396  elicc4abs  11613  caubnd2  11636  maxabsle  11723  maxabslemval  11727  maxcl  11729  mulcn2  11831  climserle  11864  fsumrecl  11920  mertenslem2  12055  ege2le3  12190  eftlub  12209  efgt1  12216  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem16  12810  xmeter  15118  bl2ioo  15232  ioo2bl  15233  ioo2blex  15234  blssioo  15235  tangtx  15520  relogmul  15551