Theorem readdcl 7458

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1438  (class class class)co 5644  ℝcr 7339   + caddc 7343

This theorem was proved from axioms:  ax-addrcl 7432

This theorem is referenced by:  0re  7478  readdcli  7491  readdcld  7507  axltadd  7546  peano2re  7608  cnegexlem3  7649  cnegex  7650  resubcl  7736  ltleadd  7914  ltaddsublt  8038  recexap  8112  recreclt  8351  cju  8411  nnge1  8435  addltmul  8642  avglt1  8644  avglt2  8645  avgle1  8646  avgle2  8647  nzadd  8792  irradd  9121  rpaddcl  9147  iooshf  9360  ge0addcl  9389  icoshft  9397  icoshftf1o  9398  iccshftr  9401  difelfznle  9534  elfzodifsumelfzo  9600  subfzo0  9641  serfre  9889  isermono  9894  ser3ge0  9940  bernneq  10062  faclbnd6  10140  readd  10291  imadd  10299  elicc4abs  10515  caubnd2  10538  maxabsle  10625  maxabslemval  10629  maxcl  10631  mulcn2  10688  climserle  10721  fsumrecl  10782  mertenslem2  10917  ege2le3  10948  eftlub  10967  efgt1  10974