Theorem readdcld 8056

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 8005	. 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 2167  (class class class)co 5922   RRcr 7878   + caddc 7882

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

This theorem is referenced by:  ltadd2  8446  leadd1  8457  le2add  8471  lt2add  8472  lesub2  8484  ltsub2  8486  gt0add  8600  reapadd1  8623  apadd1  8635  mulext1  8639  recexaplem2  8679  recp1lt1  8926  cju  8988  peano5nni  8993  peano2nn  9002  div4p1lem1div2  9245  peano2z  9362  difgtsumgt  9395  addlelt  9843  xaddf  9919  xaddval  9920  xleaddadd  9962  zltaddlt1le  10082  zssinfcl  10322  exbtwnzlemstep  10337  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnrelemcalc  10345  flqaddz  10387  btwnzge0  10390  2tnp1ge0ge0  10391  flhalf  10392  modqltm1p1mod  10468  expnbnd  10755  nn0opthlem2d  10813  remim  11025  remullem  11036  caucvgrelemcau  11145  caucvgre  11146  cvg1nlemcxze  11147  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniqlem  11159  resqrexlem1arp  11170  resqrexlemp1rp  11171  resqrexlemf1  11173  resqrexlemfp1  11174  resqrexlemover  11175  resqrexlemdec  11176  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  abs00ap  11227  absext  11228  absrele  11248  abstri  11269  abs3lem  11276  amgm2  11283  qdenre  11367  maxabsle  11369  maxabslemlub  11372  maxabslemval  11373  maxcl  11375  maxltsup  11383  bdtrilem  11404  bdtri  11405  xrbdtri  11441  mulcn2  11477  fsumabs  11630  cvgratnnlembern  11688  eirraplem  11942  ltoddhalfle  12058  divalglemnqt  12085  4sqlem12  12571  4sqlem15  12574  4sqlem16  12575  2expltfac  12608  xblss2ps  14640  cnopnap  14847  maxcncf  14851  mincncf  14852  ivthinclemlopn  14872  ivthinclemuopn  14874  hoverb  14884  ivthdichlem  14887  limcimolemlt  14900  efltlemlt  15010  cosq23lt0  15069  cosordlem  15085  lgsdirprm  15275  gausslemma2dlem1a  15299  2sqlem8  15364  qdencn  15671  trilpolemeq1  15684