Theorem readdcld 8303

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 8253	. 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 6050   RRcr 8126   + caddc 8130

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

This theorem is referenced by:  ltadd2  8693  leadd1  8704  le2add  8718  lt2add  8719  lesub2  8731  ltsub2  8733  gt0add  8847  reapadd1  8870  apadd1  8882  mulext1  8886  recexaplem2  8926  recp1lt1  9173  cju  9235  peano5nni  9240  peano2nn  9249  div4p1lem1div2  9492  peano2z  9613  difgtsumgt  9647  eluzmn  9860  addlelt  10101  xaddf  10177  xaddval  10178  xleaddadd  10220  lincmble  10337  zltaddlt1le  10341  elincfzoext  10538  zssinfcl  10592  exbtwnzlemstep  10607  exbtwnz  10610  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnrelemcalc  10615  flqaddz  10657  btwnzge0  10660  2tnp1ge0ge0  10661  flhalf  10662  modqltm1p1mod  10738  expnbnd  11025  nn0opthlem2d  11083  ccatalpha  11301  remim  11545  remullem  11556  caucvgrelemcau  11665  caucvgre  11666  cvg1nlemcxze  11667  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniqlem  11679  resqrexlem1arp  11690  resqrexlemp1rp  11691  resqrexlemf1  11693  resqrexlemfp1  11694  resqrexlemover  11695  resqrexlemdec  11696  resqrexlemlo  11698  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  abs00ap  11747  absext  11748  absrele  11768  abstri  11789  abs3lem  11796  amgm2  11803  qdenre  11887  maxabsle  11889  maxabslemlub  11892  maxabslemval  11893  maxcl  11895  maxltsup  11903  bdtrilem  11924  bdtri  11925  xrbdtri  11961  mulcn2  11997  fsumabs  12151  cvgratnnlembern  12209  eirraplem  12463  ltoddhalfle  12579  divalglemnqt  12606  bitscmp  12644  4sqlem12  13100  4sqlem15  13103  4sqlem16  13104  2expltfac  13137  xblss2ps  15269  cnopnap  15476  maxcncf  15480  mincncf  15481  ivthinclemlopn  15501  ivthinclemuopn  15503  hoverb  15513  ivthdichlem  15516  limcimolemlt  15529  efltlemlt  15639  cosq23lt0  15698  cosordlem  15714  pellexlem2  15846  lgsdirprm  15907  gausslemma2dlem1a  15931  2sqlem8  15996  qdencn  16807  repiecelem  16809  trilpolemeq1  16824