Theorem readdcl 8093

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

Assertion

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

Proof of Theorem readdcl

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2180  (class class class)co 5974  ℝcr 7966   + caddc 7970

This theorem was proved from axioms:  ax-addrcl 8064

This theorem is referenced by:  0re  8114  readdcli  8127  readdcld  8144  axltadd  8184  peano2re  8250  cnegexlem3  8291  cnegex  8292  resubcl  8378  ltleadd  8561  ltaddsublt  8686  recexap  8768  recreclt  9015  cju  9076  nnge1  9101  addltmul  9316  avglt1  9318  avglt2  9319  avgle1  9320  avgle2  9321  nzadd  9467  irradd  9809  rpaddcl  9841  xaddnemnf  10021  xaddnepnf  10022  xnegdi  10032  xaddass  10033  xltadd1  10040  iooshf  10116  ge0addcl  10145  icoshft  10154  icoshftf1o  10155  iccshftr  10158  difelfznle  10299  elfzodifsumelfzo  10374  subfzo0  10415  serfre  10673  ser3mono  10676  ser3ge0  10725  bernneq  10849  faclbnd6  10933  ccatsymb  11103  swrdswrdlem  11202  swrdccatin2  11227  readd  11346  imadd  11354  elicc4abs  11571  caubnd2  11594  maxabsle  11681  maxabslemval  11685  maxcl  11687  mulcn2  11789  climserle  11822  fsumrecl  11878  mertenslem2  12013  ege2le3  12148  eftlub  12167  efgt1  12174  pythagtriplem12  12764  pythagtriplem14  12766  pythagtriplem16  12768  xmeter  15075  bl2ioo  15189  ioo2bl  15190  ioo2blex  15191  blssioo  15192  tangtx  15477  relogmul  15508