Theorem readdcld 8302

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 8252	. 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 2203  (class class class)co 6049   RRcr 8125   + caddc 8129

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

This theorem is referenced by:  ltadd2  8692  leadd1  8703  le2add  8717  lt2add  8718  lesub2  8730  ltsub2  8732  gt0add  8846  reapadd1  8869  apadd1  8881  mulext1  8885  recexaplem2  8925  recp1lt1  9172  cju  9234  peano5nni  9239  peano2nn  9248  div4p1lem1div2  9491  peano2z  9612  difgtsumgt  9646  eluzmn  9859  addlelt  10100  xaddf  10176  xaddval  10177  xleaddadd  10219  lincmble  10336  zltaddlt1le  10340  elincfzoext  10537  zssinfcl  10591  exbtwnzlemstep  10606  exbtwnz  10609  rebtwn2zlemstep  10611  rebtwn2z  10613  qbtwnrelemcalc  10614  flqaddz  10656  btwnzge0  10659  2tnp1ge0ge0  10660  flhalf  10661  modqltm1p1mod  10737  expnbnd  11024  nn0opthlem2d  11082  ccatalpha  11297  remim  11541  remullem  11552  caucvgrelemcau  11661  caucvgre  11662  cvg1nlemcxze  11663  cvg1nlemcau  11665  cvg1nlemres  11666  recvguniqlem  11675  resqrexlem1arp  11686  resqrexlemp1rp  11687  resqrexlemf1  11689  resqrexlemfp1  11690  resqrexlemover  11691  resqrexlemdec  11692  resqrexlemlo  11694  resqrexlemcalc1  11695  resqrexlemcalc2  11696  resqrexlemnm  11699  resqrexlemcvg  11700  resqrexlemoverl  11702  resqrexlemglsq  11703  resqrexlemga  11704  abs00ap  11743  absext  11744  absrele  11764  abstri  11785  abs3lem  11792  amgm2  11799  qdenre  11883  maxabsle  11885  maxabslemlub  11888  maxabslemval  11889  maxcl  11891  maxltsup  11899  bdtrilem  11920  bdtri  11921  xrbdtri  11957  mulcn2  11993  fsumabs  12147  cvgratnnlembern  12205  eirraplem  12459  ltoddhalfle  12575  divalglemnqt  12602  bitscmp  12640  4sqlem12  13096  4sqlem15  13099  4sqlem16  13100  2expltfac  13133  xblss2ps  15261  cnopnap  15468  maxcncf  15472  mincncf  15473  ivthinclemlopn  15493  ivthinclemuopn  15495  hoverb  15505  ivthdichlem  15508  limcimolemlt  15521  efltlemlt  15631  cosq23lt0  15690  cosordlem  15706  pellexlem2  15838  lgsdirprm  15899  gausslemma2dlem1a  15923  2sqlem8  15988  qdencn  16799  repiecelem  16801  trilpolemeq1  16816