Theorem readdcld 7819

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

Syntax hints:   -> wi 4   e. wcel 1481  (class class class)co 5782   RRcr 7643   + caddc 7647

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

This theorem is referenced by:  ltadd2  8205  leadd1  8216  le2add  8230  lt2add  8231  lesub2  8243  ltsub2  8245  gt0add  8359  reapadd1  8382  apadd1  8394  mulext1  8398  recexaplem2  8437  recp1lt1  8681  cju  8743  peano5nni  8747  peano2nn  8756  div4p1lem1div2  8997  peano2z  9114  addlelt  9585  xaddf  9657  xaddval  9658  xleaddadd  9700  zltaddlt1le  9820  exbtwnzlemstep  10056  exbtwnz  10059  rebtwn2zlemstep  10061  rebtwn2z  10063  qbtwnrelemcalc  10064  flqaddz  10101  btwnzge0  10104  2tnp1ge0ge0  10105  flhalf  10106  modqltm1p1mod  10180  expnbnd  10446  nn0opthlem2d  10499  remim  10664  remullem  10675  caucvgrelemcau  10784  caucvgre  10785  cvg1nlemcxze  10786  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniqlem  10798  resqrexlem1arp  10809  resqrexlemp1rp  10810  resqrexlemf1  10812  resqrexlemfp1  10813  resqrexlemover  10814  resqrexlemdec  10815  resqrexlemlo  10817  resqrexlemcalc1  10818  resqrexlemcalc2  10819  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  abs00ap  10866  absext  10867  absrele  10887  abstri  10908  abs3lem  10915  amgm2  10922  qdenre  11006  maxabsle  11008  maxabslemlub  11011  maxabslemval  11012  maxcl  11014  maxltsup  11022  bdtrilem  11042  bdtri  11043  xrbdtri  11077  mulcn2  11113  fsumabs  11266  cvgratnnlembern  11324  eirraplem  11519  ltoddhalfle  11626  divalglemnqt  11653  zssinfcl  11677  xblss2ps  12612  cnopnap  12802  ivthinclemlopn  12822  ivthinclemuopn  12824  limcimolemlt  12841  efltlemlt  12903  cosq23lt0  12962  cosordlem  12978  qdencn  13397  trilpolemeq1  13408