Theorem readdcld 8319

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 8269	. 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 2205  (class class class)co 6058   RRcr 8142   + caddc 8146

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

This theorem is referenced by:  ltadd2  8710  leadd1  8721  le2add  8735  lt2add  8736  lesub2  8748  ltsub2  8750  gt0add  8864  reapadd1  8887  apadd1  8899  mulext1  8903  recexaplem2  8943  recp1lt1  9190  cju  9252  peano5nni  9257  peano2nn  9266  div4p1lem1div2  9509  peano2z  9630  difgtsumgt  9664  eluzmn  9878  addlelt  10119  xaddf  10196  xaddval  10197  xleaddadd  10239  lincmble  10356  zltaddlt1le  10360  elincfzoext  10560  zssinfcl  10614  exbtwnzlemstep  10631  exbtwnz  10634  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnrelemcalc  10639  flqaddz  10681  btwnzge0  10684  2tnp1ge0ge0  10685  flhalf  10686  modqltm1p1mod  10762  expnbnd  11050  nn0opthlem2d  11108  ccatalpha  11326  remim  11570  remullem  11581  caucvgrelemcau  11690  caucvgre  11691  cvg1nlemcxze  11692  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniqlem  11704  resqrexlem1arp  11715  resqrexlemp1rp  11716  resqrexlemf1  11718  resqrexlemfp1  11719  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemlo  11723  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  abs00ap  11772  absext  11773  absrele  11793  abstri  11814  abs3lem  11821  amgm2  11828  qdenre  11912  maxabsle  11914  maxabslemlub  11917  maxabslemval  11918  maxcl  11920  maxltsup  11928  bdtrilem  11949  bdtri  11950  xrbdtri  11986  mulcn2  12022  fsumabs  12176  cvgratnnlembern  12234  eirraplem  12488  ltoddhalfle  12604  divalglemnqt  12631  bitscmp  12669  4sqlem12  13125  4sqlem15  13128  4sqlem16  13129  2expltfac  13162  ballotfilemsgt1  13198  ballotfilemsel1i  13200  xblss2ps  15395  cnopnap  15602  maxcncf  15606  mincncf  15607  ivthinclemlopn  15627  ivthinclemuopn  15629  hoverb  15639  ivthdichlem  15642  limcimolemlt  15655  efltlemlt  15765  cosq23lt0  15824  cosordlem  15840  pellexlem2  15972  lgsdirprm  16033  gausslemma2dlem1a  16057  2sqlem8  16122  qdencn  16933  repiecelem  16935  trilpolemeq1  16950