Theorem readdcl 7875

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136  (class class class)co 5841  ℝcr 7748   + caddc 7752

This theorem was proved from axioms:  ax-addrcl 7846

This theorem is referenced by:  0re  7895  readdcli  7908  readdcld  7924  axltadd  7964  peano2re  8030  cnegexlem3  8071  cnegex  8072  resubcl  8158  ltleadd  8340  ltaddsublt  8465  recexap  8546  recreclt  8791  cju  8852  nnge1  8876  addltmul  9089  avglt1  9091  avglt2  9092  avgle1  9093  avgle2  9094  nzadd  9239  irradd  9580  rpaddcl  9609  xaddnemnf  9789  xaddnepnf  9790  xnegdi  9800  xaddass  9801  xltadd1  9808  iooshf  9884  ge0addcl  9913  icoshft  9922  icoshftf1o  9923  iccshftr  9926  difelfznle  10066  elfzodifsumelfzo  10132  subfzo0  10173  serfre  10406  ser3mono  10409  ser3ge0  10448  bernneq  10571  faclbnd6  10653  readd  10807  imadd  10815  elicc4abs  11032  caubnd2  11055  maxabsle  11142  maxabslemval  11146  maxcl  11148  mulcn2  11249  climserle  11282  fsumrecl  11338  mertenslem2  11473  ege2le3  11608  eftlub  11627  efgt1  11634  pythagtriplem12  12203  pythagtriplem14  12205  pythagtriplem16  12207  xmeter  13036  bl2ioo  13142  ioo2bl  13143  ioo2blex  13144  blssioo  13145  tangtx  13359  relogmul  13390