Theorem readdcl 7753

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  (class class class)co 5774  ℝcr 7626   + caddc 7630

This theorem was proved from axioms:  ax-addrcl 7724

This theorem is referenced by:  0re  7773  readdcli  7786  readdcld  7802  axltadd  7841  peano2re  7905  cnegexlem3  7946  cnegex  7947  resubcl  8033  ltleadd  8215  ltaddsublt  8340  recexap  8421  recreclt  8665  cju  8726  nnge1  8750  addltmul  8963  avglt1  8965  avglt2  8966  avgle1  8967  avgle2  8968  nzadd  9113  irradd  9445  rpaddcl  9472  xaddnemnf  9647  xaddnepnf  9648  xnegdi  9658  xaddass  9659  xltadd1  9666  iooshf  9742  ge0addcl  9771  icoshft  9780  icoshftf1o  9781  iccshftr  9784  difelfznle  9919  elfzodifsumelfzo  9985  subfzo0  10026  serfre  10255  ser3mono  10258  ser3ge0  10297  bernneq  10419  faclbnd6  10497  readd  10648  imadd  10656  elicc4abs  10873  caubnd2  10896  maxabsle  10983  maxabslemval  10987  maxcl  10989  mulcn2  11088  climserle  11121  fsumrecl  11177  mertenslem2  11312  ege2le3  11384  eftlub  11403  efgt1  11410  xmeter  12615  bl2ioo  12721  ioo2bl  12722  ioo2blex  12723  blssioo  12724  tangtx  12929