Theorem readdcld 8172

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 8121	. 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 2200  (class class class)co 6000   RRcr 7994   + caddc 7998

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

This theorem is referenced by:  ltadd2  8562  leadd1  8573  le2add  8587  lt2add  8588  lesub2  8600  ltsub2  8602  gt0add  8716  reapadd1  8739  apadd1  8751  mulext1  8755  recexaplem2  8795  recp1lt1  9042  cju  9104  peano5nni  9109  peano2nn  9118  div4p1lem1div2  9361  peano2z  9478  difgtsumgt  9512  addlelt  9960  xaddf  10036  xaddval  10037  xleaddadd  10079  zltaddlt1le  10199  elincfzoext  10394  zssinfcl  10447  exbtwnzlemstep  10462  exbtwnz  10465  rebtwn2zlemstep  10467  rebtwn2z  10469  qbtwnrelemcalc  10470  flqaddz  10512  btwnzge0  10515  2tnp1ge0ge0  10516  flhalf  10517  modqltm1p1mod  10593  expnbnd  10880  nn0opthlem2d  10938  remim  11366  remullem  11377  caucvgrelemcau  11486  caucvgre  11487  cvg1nlemcxze  11488  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniqlem  11500  resqrexlem1arp  11511  resqrexlemp1rp  11512  resqrexlemf1  11514  resqrexlemfp1  11515  resqrexlemover  11516  resqrexlemdec  11517  resqrexlemlo  11519  resqrexlemcalc1  11520  resqrexlemcalc2  11521  resqrexlemnm  11524  resqrexlemcvg  11525  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  abs00ap  11568  absext  11569  absrele  11589  abstri  11610  abs3lem  11617  amgm2  11624  qdenre  11708  maxabsle  11710  maxabslemlub  11713  maxabslemval  11714  maxcl  11716  maxltsup  11724  bdtrilem  11745  bdtri  11746  xrbdtri  11782  mulcn2  11818  fsumabs  11971  cvgratnnlembern  12029  eirraplem  12283  ltoddhalfle  12399  divalglemnqt  12426  bitscmp  12464  4sqlem12  12920  4sqlem15  12923  4sqlem16  12924  2expltfac  12957  xblss2ps  15072  cnopnap  15279  maxcncf  15283  mincncf  15284  ivthinclemlopn  15304  ivthinclemuopn  15306  hoverb  15316  ivthdichlem  15319  limcimolemlt  15332  efltlemlt  15442  cosq23lt0  15501  cosordlem  15517  lgsdirprm  15707  gausslemma2dlem1a  15731  2sqlem8  15796  qdencn  16354  trilpolemeq1  16367