Theorem readdcld 8101

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 8050	. 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 2175  (class class class)co 5943   RRcr 7923   + caddc 7927

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

This theorem is referenced by:  ltadd2  8491  leadd1  8502  le2add  8516  lt2add  8517  lesub2  8529  ltsub2  8531  gt0add  8645  reapadd1  8668  apadd1  8680  mulext1  8684  recexaplem2  8724  recp1lt1  8971  cju  9033  peano5nni  9038  peano2nn  9047  div4p1lem1div2  9290  peano2z  9407  difgtsumgt  9441  addlelt  9889  xaddf  9965  xaddval  9966  xleaddadd  10008  zltaddlt1le  10128  elincfzoext  10320  zssinfcl  10373  exbtwnzlemstep  10388  exbtwnz  10391  rebtwn2zlemstep  10393  rebtwn2z  10395  qbtwnrelemcalc  10396  flqaddz  10438  btwnzge0  10441  2tnp1ge0ge0  10442  flhalf  10443  modqltm1p1mod  10519  expnbnd  10806  nn0opthlem2d  10864  remim  11142  remullem  11153  caucvgrelemcau  11262  caucvgre  11263  cvg1nlemcxze  11264  cvg1nlemcau  11266  cvg1nlemres  11267  recvguniqlem  11276  resqrexlem1arp  11287  resqrexlemp1rp  11288  resqrexlemf1  11290  resqrexlemfp1  11291  resqrexlemover  11292  resqrexlemdec  11293  resqrexlemlo  11295  resqrexlemcalc1  11296  resqrexlemcalc2  11297  resqrexlemnm  11300  resqrexlemcvg  11301  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemga  11305  abs00ap  11344  absext  11345  absrele  11365  abstri  11386  abs3lem  11393  amgm2  11400  qdenre  11484  maxabsle  11486  maxabslemlub  11489  maxabslemval  11490  maxcl  11492  maxltsup  11500  bdtrilem  11521  bdtri  11522  xrbdtri  11558  mulcn2  11594  fsumabs  11747  cvgratnnlembern  11805  eirraplem  12059  ltoddhalfle  12175  divalglemnqt  12202  bitscmp  12240  4sqlem12  12696  4sqlem15  12699  4sqlem16  12700  2expltfac  12733  xblss2ps  14847  cnopnap  15054  maxcncf  15058  mincncf  15059  ivthinclemlopn  15079  ivthinclemuopn  15081  hoverb  15091  ivthdichlem  15094  limcimolemlt  15107  efltlemlt  15217  cosq23lt0  15276  cosordlem  15292  lgsdirprm  15482  gausslemma2dlem1a  15506  2sqlem8  15571  qdencn  15928  trilpolemeq1  15941