Theorem readdcld 8051

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 8000	. 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 2164  (class class class)co 5919   RRcr 7873   + caddc 7877

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

This theorem is referenced by:  ltadd2  8440  leadd1  8451  le2add  8465  lt2add  8466  lesub2  8478  ltsub2  8480  gt0add  8594  reapadd1  8617  apadd1  8629  mulext1  8633  recexaplem2  8673  recp1lt1  8920  cju  8982  peano5nni  8987  peano2nn  8996  div4p1lem1div2  9239  peano2z  9356  difgtsumgt  9389  addlelt  9837  xaddf  9913  xaddval  9914  xleaddadd  9956  zltaddlt1le  10076  exbtwnzlemstep  10319  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnrelemcalc  10327  flqaddz  10369  btwnzge0  10372  2tnp1ge0ge0  10373  flhalf  10374  modqltm1p1mod  10450  expnbnd  10737  nn0opthlem2d  10795  remim  11007  remullem  11018  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemcxze  11129  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniqlem  11141  resqrexlem1arp  11152  resqrexlemp1rp  11153  resqrexlemf1  11155  resqrexlemfp1  11156  resqrexlemover  11157  resqrexlemdec  11158  resqrexlemlo  11160  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  abs00ap  11209  absext  11210  absrele  11230  abstri  11251  abs3lem  11258  amgm2  11265  qdenre  11349  maxabsle  11351  maxabslemlub  11354  maxabslemval  11355  maxcl  11357  maxltsup  11365  bdtrilem  11385  bdtri  11386  xrbdtri  11422  mulcn2  11458  fsumabs  11611  cvgratnnlembern  11669  eirraplem  11923  ltoddhalfle  12037  divalglemnqt  12064  zssinfcl  12088  4sqlem12  12543  4sqlem15  12546  4sqlem16  12547  xblss2ps  14583  cnopnap  14790  maxcncf  14794  mincncf  14795  ivthinclemlopn  14815  ivthinclemuopn  14817  hoverb  14827  ivthdichlem  14830  limcimolemlt  14843  efltlemlt  14950  cosq23lt0  15009  cosordlem  15025  lgsdirprm  15191  gausslemma2dlem1a  15215  2sqlem8  15280  qdencn  15587  trilpolemeq1  15600