Theorem readdcld 8132

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 8081	. 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 2177  (class class class)co 5962   RRcr 7954   + caddc 7958

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

This theorem is referenced by:  ltadd2  8522  leadd1  8533  le2add  8547  lt2add  8548  lesub2  8560  ltsub2  8562  gt0add  8676  reapadd1  8699  apadd1  8711  mulext1  8715  recexaplem2  8755  recp1lt1  9002  cju  9064  peano5nni  9069  peano2nn  9078  div4p1lem1div2  9321  peano2z  9438  difgtsumgt  9472  addlelt  9920  xaddf  9996  xaddval  9997  xleaddadd  10039  zltaddlt1le  10159  elincfzoext  10354  zssinfcl  10407  exbtwnzlemstep  10422  exbtwnz  10425  rebtwn2zlemstep  10427  rebtwn2z  10429  qbtwnrelemcalc  10430  flqaddz  10472  btwnzge0  10475  2tnp1ge0ge0  10476  flhalf  10477  modqltm1p1mod  10553  expnbnd  10840  nn0opthlem2d  10898  remim  11256  remullem  11267  caucvgrelemcau  11376  caucvgre  11377  cvg1nlemcxze  11378  cvg1nlemcau  11380  cvg1nlemres  11381  recvguniqlem  11390  resqrexlem1arp  11401  resqrexlemp1rp  11402  resqrexlemf1  11404  resqrexlemfp1  11405  resqrexlemover  11406  resqrexlemdec  11407  resqrexlemlo  11409  resqrexlemcalc1  11410  resqrexlemcalc2  11411  resqrexlemnm  11414  resqrexlemcvg  11415  resqrexlemoverl  11417  resqrexlemglsq  11418  resqrexlemga  11419  abs00ap  11458  absext  11459  absrele  11479  abstri  11500  abs3lem  11507  amgm2  11514  qdenre  11598  maxabsle  11600  maxabslemlub  11603  maxabslemval  11604  maxcl  11606  maxltsup  11614  bdtrilem  11635  bdtri  11636  xrbdtri  11672  mulcn2  11708  fsumabs  11861  cvgratnnlembern  11919  eirraplem  12173  ltoddhalfle  12289  divalglemnqt  12316  bitscmp  12354  4sqlem12  12810  4sqlem15  12813  4sqlem16  12814  2expltfac  12847  xblss2ps  14961  cnopnap  15168  maxcncf  15172  mincncf  15173  ivthinclemlopn  15193  ivthinclemuopn  15195  hoverb  15205  ivthdichlem  15208  limcimolemlt  15221  efltlemlt  15331  cosq23lt0  15390  cosordlem  15406  lgsdirprm  15596  gausslemma2dlem1a  15620  2sqlem8  15685  qdencn  16138  trilpolemeq1  16151