Theorem readdcl 8071

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

Assertion

Ref	Expression
readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 8042	1 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2177  (class class class)co 5957   RRcr 7944   + caddc 7948

This theorem was proved from axioms:  ax-addrcl 8042

This theorem is referenced by:  0re  8092  readdcli  8105  readdcld  8122  axltadd  8162  peano2re  8228  cnegexlem3  8269  cnegex  8270  resubcl  8356  ltleadd  8539  ltaddsublt  8664  recexap  8746  recreclt  8993  cju  9054  nnge1  9079  addltmul  9294  avglt1  9296  avglt2  9297  avgle1  9298  avgle2  9299  nzadd  9445  irradd  9787  rpaddcl  9819  xaddnemnf  9999  xaddnepnf  10000  xnegdi  10010  xaddass  10011  xltadd1  10018  iooshf  10094  ge0addcl  10123  icoshft  10132  icoshftf1o  10133  iccshftr  10136  difelfznle  10277  elfzodifsumelfzo  10352  subfzo0  10393  serfre  10651  ser3mono  10654  ser3ge0  10703  bernneq  10827  faclbnd6  10911  ccatsymb  11081  swrdswrdlem  11180  readd  11255  imadd  11263  elicc4abs  11480  caubnd2  11503  maxabsle  11590  maxabslemval  11594  maxcl  11596  mulcn2  11698  climserle  11731  fsumrecl  11787  mertenslem2  11922  ege2le3  12057  eftlub  12076  efgt1  12083  pythagtriplem12  12673  pythagtriplem14  12675  pythagtriplem16  12677  xmeter  14983  bl2ioo  15097  ioo2bl  15098  ioo2blex  15099  blssioo  15100  tangtx  15385  relogmul  15416