Theorem readdcld 8208

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 8157	. 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 2202  (class class class)co 6017   RRcr 8030   + caddc 8034

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

This theorem is referenced by:  ltadd2  8598  leadd1  8609  le2add  8623  lt2add  8624  lesub2  8636  ltsub2  8638  gt0add  8752  reapadd1  8775  apadd1  8787  mulext1  8791  recexaplem2  8831  recp1lt1  9078  cju  9140  peano5nni  9145  peano2nn  9154  div4p1lem1div2  9397  peano2z  9514  difgtsumgt  9548  eluzmn  9761  addlelt  10002  xaddf  10078  xaddval  10079  xleaddadd  10121  zltaddlt1le  10241  elincfzoext  10437  zssinfcl  10491  exbtwnzlemstep  10506  exbtwnz  10509  rebtwn2zlemstep  10511  rebtwn2z  10513  qbtwnrelemcalc  10514  flqaddz  10556  btwnzge0  10559  2tnp1ge0ge0  10560  flhalf  10561  modqltm1p1mod  10637  expnbnd  10924  nn0opthlem2d  10982  ccatalpha  11189  remim  11420  remullem  11431  caucvgrelemcau  11540  caucvgre  11541  cvg1nlemcxze  11542  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniqlem  11554  resqrexlem1arp  11565  resqrexlemp1rp  11566  resqrexlemf1  11568  resqrexlemfp1  11569  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemlo  11573  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  abs00ap  11622  absext  11623  absrele  11643  abstri  11664  abs3lem  11671  amgm2  11678  qdenre  11762  maxabsle  11764  maxabslemlub  11767  maxabslemval  11768  maxcl  11770  maxltsup  11778  bdtrilem  11799  bdtri  11800  xrbdtri  11836  mulcn2  11872  fsumabs  12025  cvgratnnlembern  12083  eirraplem  12337  ltoddhalfle  12453  divalglemnqt  12480  bitscmp  12518  4sqlem12  12974  4sqlem15  12977  4sqlem16  12978  2expltfac  13011  xblss2ps  15127  cnopnap  15334  maxcncf  15338  mincncf  15339  ivthinclemlopn  15359  ivthinclemuopn  15361  hoverb  15371  ivthdichlem  15374  limcimolemlt  15387  efltlemlt  15497  cosq23lt0  15556  cosordlem  15572  lgsdirprm  15762  gausslemma2dlem1a  15786  2sqlem8  15851  qdencn  16631  trilpolemeq1  16644