Theorem readdcl 7939

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812   + caddc 7816

This theorem was proved from axioms:  ax-addrcl 7910

This theorem is referenced by:  0re  7959  readdcli  7972  readdcld  7989  axltadd  8029  peano2re  8095  cnegexlem3  8136  cnegex  8137  resubcl  8223  ltleadd  8405  ltaddsublt  8530  recexap  8612  recreclt  8859  cju  8920  nnge1  8944  addltmul  9157  avglt1  9159  avglt2  9160  avgle1  9161  avgle2  9162  nzadd  9307  irradd  9648  rpaddcl  9679  xaddnemnf  9859  xaddnepnf  9860  xnegdi  9870  xaddass  9871  xltadd1  9878  iooshf  9954  ge0addcl  9983  icoshft  9992  icoshftf1o  9993  iccshftr  9996  difelfznle  10137  elfzodifsumelfzo  10203  subfzo0  10244  serfre  10477  ser3mono  10480  ser3ge0  10519  bernneq  10643  faclbnd6  10726  readd  10880  imadd  10888  elicc4abs  11105  caubnd2  11128  maxabsle  11215  maxabslemval  11219  maxcl  11221  mulcn2  11322  climserle  11355  fsumrecl  11411  mertenslem2  11546  ege2le3  11681  eftlub  11700  efgt1  11707  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem16  12281  xmeter  13975  bl2ioo  14081  ioo2bl  14082  ioo2blex  14083  blssioo  14084  tangtx  14298  relogmul  14329