Theorem readdcld 8102

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	|- ( ph -> A e. RR )
readdcld.2	|- ( ph -> B e. RR )

Assertion

Ref	Expression
readdcld	|- ( ph -> ( A + B ) e. RR )

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		readdcld.2	. 2 |- ( ph -> B e. RR )
3		readdcl 8051	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2176  (class class class)co 5944   RRcr 7924   + caddc 7928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-addrcl 8022

This theorem is referenced by:  ltadd2  8492  leadd1  8503  le2add  8517  lt2add  8518  lesub2  8530  ltsub2  8532  gt0add  8646  reapadd1  8669  apadd1  8681  mulext1  8685  recexaplem2  8725  recp1lt1  8972  cju  9034  peano5nni  9039  peano2nn  9048  div4p1lem1div2  9291  peano2z  9408  difgtsumgt  9442  addlelt  9890  xaddf  9966  xaddval  9967  xleaddadd  10009  zltaddlt1le  10129  elincfzoext  10322  zssinfcl  10375  exbtwnzlemstep  10390  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2z  10397  qbtwnrelemcalc  10398  flqaddz  10440  btwnzge0  10443  2tnp1ge0ge0  10444  flhalf  10445  modqltm1p1mod  10521  expnbnd  10808  nn0opthlem2d  10866  remim  11171  remullem  11182  caucvgrelemcau  11291  caucvgre  11292  cvg1nlemcxze  11293  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniqlem  11305  resqrexlem1arp  11316  resqrexlemp1rp  11317  resqrexlemf1  11319  resqrexlemfp1  11320  resqrexlemover  11321  resqrexlemdec  11322  resqrexlemlo  11324  resqrexlemcalc1  11325  resqrexlemcalc2  11326  resqrexlemnm  11329  resqrexlemcvg  11330  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemga  11334  abs00ap  11373  absext  11374  absrele  11394  abstri  11415  abs3lem  11422  amgm2  11429  qdenre  11513  maxabsle  11515  maxabslemlub  11518  maxabslemval  11519  maxcl  11521  maxltsup  11529  bdtrilem  11550  bdtri  11551  xrbdtri  11587  mulcn2  11623  fsumabs  11776  cvgratnnlembern  11834  eirraplem  12088  ltoddhalfle  12204  divalglemnqt  12231  bitscmp  12269  4sqlem12  12725  4sqlem15  12728  4sqlem16  12729  2expltfac  12762  xblss2ps  14876  cnopnap  15083  maxcncf  15087  mincncf  15088  ivthinclemlopn  15108  ivthinclemuopn  15110  hoverb  15120  ivthdichlem  15123  limcimolemlt  15136  efltlemlt  15246  cosq23lt0  15305  cosordlem  15321  lgsdirprm  15511  gausslemma2dlem1a  15535  2sqlem8  15600  qdencn  15966  trilpolemeq1  15979