Theorem readdcld 7987

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 7937	. 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 2148  (class class class)co 5875   RRcr 7810   + caddc 7814

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

This theorem is referenced by:  ltadd2  8376  leadd1  8387  le2add  8401  lt2add  8402  lesub2  8414  ltsub2  8416  gt0add  8530  reapadd1  8553  apadd1  8565  mulext1  8569  recexaplem2  8609  recp1lt1  8856  cju  8918  peano5nni  8922  peano2nn  8931  div4p1lem1div2  9172  peano2z  9289  difgtsumgt  9322  addlelt  9768  xaddf  9844  xaddval  9845  xleaddadd  9887  zltaddlt1le  10007  exbtwnzlemstep  10248  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnrelemcalc  10256  flqaddz  10297  btwnzge0  10300  2tnp1ge0ge0  10301  flhalf  10302  modqltm1p1mod  10376  expnbnd  10644  nn0opthlem2d  10701  remim  10869  remullem  10880  caucvgrelemcau  10989  caucvgre  10990  cvg1nlemcxze  10991  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniqlem  11003  resqrexlem1arp  11014  resqrexlemp1rp  11015  resqrexlemf1  11017  resqrexlemfp1  11018  resqrexlemover  11019  resqrexlemdec  11020  resqrexlemlo  11022  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemoverl  11030  resqrexlemglsq  11031  resqrexlemga  11032  abs00ap  11071  absext  11072  absrele  11092  abstri  11113  abs3lem  11120  amgm2  11127  qdenre  11211  maxabsle  11213  maxabslemlub  11216  maxabslemval  11217  maxcl  11219  maxltsup  11227  bdtrilem  11247  bdtri  11248  xrbdtri  11284  mulcn2  11320  fsumabs  11473  cvgratnnlembern  11531  eirraplem  11784  ltoddhalfle  11898  divalglemnqt  11925  zssinfcl  11949  xblss2ps  13907  cnopnap  14097  ivthinclemlopn  14117  ivthinclemuopn  14119  limcimolemlt  14136  efltlemlt  14198  cosq23lt0  14257  cosordlem  14273  lgsdirprm  14438  2sqlem8  14473  qdencn  14778  trilpolemeq1  14791