Theorem readdcld 7795

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

Syntax hints:   -> wi 4   e. wcel 1480  (class class class)co 5774   RRcr 7619   + caddc 7623

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

This theorem is referenced by:  ltadd2  8181  leadd1  8192  le2add  8206  lt2add  8207  lesub2  8219  ltsub2  8221  gt0add  8335  reapadd1  8358  apadd1  8370  mulext1  8374  recexaplem2  8413  recp1lt1  8657  cju  8719  peano5nni  8723  peano2nn  8732  div4p1lem1div2  8973  peano2z  9090  addlelt  9555  xaddf  9627  xaddval  9628  xleaddadd  9670  zltaddlt1le  9789  exbtwnzlemstep  10025  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnrelemcalc  10033  flqaddz  10070  btwnzge0  10073  2tnp1ge0ge0  10074  flhalf  10075  modqltm1p1mod  10149  expnbnd  10415  nn0opthlem2d  10467  remim  10632  remullem  10643  caucvgrelemcau  10752  caucvgre  10753  cvg1nlemcxze  10754  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniqlem  10766  resqrexlem1arp  10777  resqrexlemp1rp  10778  resqrexlemf1  10780  resqrexlemfp1  10781  resqrexlemover  10782  resqrexlemdec  10783  resqrexlemlo  10785  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemga  10795  abs00ap  10834  absext  10835  absrele  10855  abstri  10876  abs3lem  10883  amgm2  10890  qdenre  10974  maxabsle  10976  maxabslemlub  10979  maxabslemval  10980  maxcl  10982  maxltsup  10990  bdtrilem  11010  bdtri  11011  xrbdtri  11045  mulcn2  11081  fsumabs  11234  cvgratnnlembern  11292  eirraplem  11483  ltoddhalfle  11590  divalglemnqt  11617  zssinfcl  11641  xblss2ps  12573  cnopnap  12763  ivthinclemlopn  12783  ivthinclemuopn  12785  limcimolemlt  12802  cosq23lt0  12914  cosordlem  12930  qdencn  13222  trilpolemeq1  13233