Theorem readdcld 8345

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 8295	. 2 |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> ( A + B ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2209  (class class class)co 6075   RRcr 8168   + caddc 8172

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

This theorem is referenced by:  ltadd2  8737  leadd1  8748  le2add  8762  lt2add  8763  lesub2  8775  ltsub2  8777  gt0add  8891  reapadd1  8914  apadd1  8926  mulext1  8930  recexaplem2  8970  recp1lt1  9219  cju  9281  peano5nni  9286  peano2nn  9295  div4p1lem1div2  9538  peano2z  9659  difgtsumgt  9693  eluzmn  9907  addlelt  10148  xaddf  10225  xaddval  10226  xleaddadd  10268  lincmble  10385  zltaddlt1le  10389  elincfzoext  10589  zssinfcl  10643  exbtwnzlemstep  10660  exbtwnz  10663  rebtwn2zlemstep  10665  rebtwn2z  10667  qbtwnrelemcalc  10668  flqaddz  10710  btwnzge0  10713  2tnp1ge0ge0  10714  flhalf  10715  modqltm1p1mod  10791  expnbnd  11079  nn0opthlem2d  11137  ccatalpha  11359  remim  11603  remullem  11614  sq01  11638  caucvgrelemcau  11724  caucvgre  11725  cvg1nlemcxze  11726  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniqlem  11738  resqrexlem1arp  11749  resqrexlemp1rp  11750  resqrexlemf1  11752  resqrexlemfp1  11753  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemlo  11757  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  abs00ap  11806  absext  11807  absrele  11827  abstri  11848  abs3lem  11855  amgm2  11862  qdenre  11946  maxabsle  11948  maxabslemlub  11951  maxabslemval  11952  maxcl  11954  maxltsup  11962  bdtrilem  11983  bdtri  11984  xrbdtri  12020  mulcn2  12056  fsumabs  12210  cvgratnnlembern  12268  eirraplem  12522  ltoddhalfle  12638  divalglemnqt  12665  bitscmp  12703  4sqlem12  13159  4sqlem15  13162  4sqlem16  13163  2expltfac  13196  ballotfilemsgt1  13232  ballotfilemsel1i  13234  xblss2ps  15428  cnopnap  15635  maxcncf  15639  mincncf  15640  ivthinclemlopn  15660  ivthinclemuopn  15662  hoverb  15672  ivthdichlem  15675  limcimolemlt  15688  efltlemlt  15798  cosq23lt0  15857  cosordlem  15873  pellexlem2  16006  lgsdirprm  16067  gausslemma2dlem1a  16091  2sqlem8  16156  qdencn  16977  repiecelem  16979  trilpolemeq1  16994