Theorem readdcld 8251

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 8201	. 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 2202  (class class class)co 6028   RRcr 8074   + caddc 8078

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

This theorem is referenced by:  ltadd2  8641  leadd1  8652  le2add  8666  lt2add  8667  lesub2  8679  ltsub2  8681  gt0add  8795  reapadd1  8818  apadd1  8830  mulext1  8834  recexaplem2  8874  recp1lt1  9121  cju  9183  peano5nni  9188  peano2nn  9197  div4p1lem1div2  9440  peano2z  9559  difgtsumgt  9593  eluzmn  9806  addlelt  10047  xaddf  10123  xaddval  10124  xleaddadd  10166  lincmble  10283  zltaddlt1le  10287  elincfzoext  10484  zssinfcl  10538  exbtwnzlemstep  10553  exbtwnz  10556  rebtwn2zlemstep  10558  rebtwn2z  10560  qbtwnrelemcalc  10561  flqaddz  10603  btwnzge0  10606  2tnp1ge0ge0  10607  flhalf  10608  modqltm1p1mod  10684  expnbnd  10971  nn0opthlem2d  11029  ccatalpha  11239  remim  11483  remullem  11494  caucvgrelemcau  11603  caucvgre  11604  cvg1nlemcxze  11605  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniqlem  11617  resqrexlem1arp  11628  resqrexlemp1rp  11629  resqrexlemf1  11631  resqrexlemfp1  11632  resqrexlemover  11633  resqrexlemdec  11634  resqrexlemlo  11636  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  abs00ap  11685  absext  11686  absrele  11706  abstri  11727  abs3lem  11734  amgm2  11741  qdenre  11825  maxabsle  11827  maxabslemlub  11830  maxabslemval  11831  maxcl  11833  maxltsup  11841  bdtrilem  11862  bdtri  11863  xrbdtri  11899  mulcn2  11935  fsumabs  12089  cvgratnnlembern  12147  eirraplem  12401  ltoddhalfle  12517  divalglemnqt  12544  bitscmp  12582  4sqlem12  13038  4sqlem15  13041  4sqlem16  13042  2expltfac  13075  xblss2ps  15198  cnopnap  15405  maxcncf  15409  mincncf  15410  ivthinclemlopn  15430  ivthinclemuopn  15432  hoverb  15442  ivthdichlem  15445  limcimolemlt  15458  efltlemlt  15568  cosq23lt0  15627  cosordlem  15643  pellexlem2  15775  lgsdirprm  15836  gausslemma2dlem1a  15860  2sqlem8  15925  qdencn  16738  repiecelem  16740  trilpolemeq1  16755