Theorem readdcld 8199

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 8148	. 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 2200  (class class class)co 6013   RRcr 8021   + caddc 8025

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

This theorem is referenced by:  ltadd2  8589  leadd1  8600  le2add  8614  lt2add  8615  lesub2  8627  ltsub2  8629  gt0add  8743  reapadd1  8766  apadd1  8778  mulext1  8782  recexaplem2  8822  recp1lt1  9069  cju  9131  peano5nni  9136  peano2nn  9145  div4p1lem1div2  9388  peano2z  9505  difgtsumgt  9539  eluzmn  9752  addlelt  9993  xaddf  10069  xaddval  10070  xleaddadd  10112  zltaddlt1le  10232  elincfzoext  10428  zssinfcl  10482  exbtwnzlemstep  10497  exbtwnz  10500  rebtwn2zlemstep  10502  rebtwn2z  10504  qbtwnrelemcalc  10505  flqaddz  10547  btwnzge0  10550  2tnp1ge0ge0  10551  flhalf  10552  modqltm1p1mod  10628  expnbnd  10915  nn0opthlem2d  10973  ccatalpha  11180  remim  11411  remullem  11422  caucvgrelemcau  11531  caucvgre  11532  cvg1nlemcxze  11533  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniqlem  11545  resqrexlem1arp  11556  resqrexlemp1rp  11557  resqrexlemf1  11559  resqrexlemfp1  11560  resqrexlemover  11561  resqrexlemdec  11562  resqrexlemlo  11564  resqrexlemcalc1  11565  resqrexlemcalc2  11566  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  abs00ap  11613  absext  11614  absrele  11634  abstri  11655  abs3lem  11662  amgm2  11669  qdenre  11753  maxabsle  11755  maxabslemlub  11758  maxabslemval  11759  maxcl  11761  maxltsup  11769  bdtrilem  11790  bdtri  11791  xrbdtri  11827  mulcn2  11863  fsumabs  12016  cvgratnnlembern  12074  eirraplem  12328  ltoddhalfle  12444  divalglemnqt  12471  bitscmp  12509  4sqlem12  12965  4sqlem15  12968  4sqlem16  12969  2expltfac  13002  xblss2ps  15118  cnopnap  15325  maxcncf  15329  mincncf  15330  ivthinclemlopn  15350  ivthinclemuopn  15352  hoverb  15362  ivthdichlem  15365  limcimolemlt  15378  efltlemlt  15488  cosq23lt0  15547  cosordlem  15563  lgsdirprm  15753  gausslemma2dlem1a  15777  2sqlem8  15842  qdencn  16567  trilpolemeq1  16580