Theorem readdcld 7961

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 7912	. 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 2146  (class class class)co 5865   RRcr 7785   + caddc 7789

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

This theorem is referenced by:  ltadd2  8350  leadd1  8361  le2add  8375  lt2add  8376  lesub2  8388  ltsub2  8390  gt0add  8504  reapadd1  8527  apadd1  8539  mulext1  8543  recexaplem2  8582  recp1lt1  8827  cju  8889  peano5nni  8893  peano2nn  8902  div4p1lem1div2  9143  peano2z  9260  difgtsumgt  9293  addlelt  9737  xaddf  9813  xaddval  9814  xleaddadd  9856  zltaddlt1le  9976  exbtwnzlemstep  10216  exbtwnz  10219  rebtwn2zlemstep  10221  rebtwn2z  10223  qbtwnrelemcalc  10224  flqaddz  10265  btwnzge0  10268  2tnp1ge0ge0  10269  flhalf  10270  modqltm1p1mod  10344  expnbnd  10611  nn0opthlem2d  10667  remim  10835  remullem  10846  caucvgrelemcau  10955  caucvgre  10956  cvg1nlemcxze  10957  cvg1nlemcau  10959  cvg1nlemres  10960  recvguniqlem  10969  resqrexlem1arp  10980  resqrexlemp1rp  10981  resqrexlemf1  10983  resqrexlemfp1  10984  resqrexlemover  10985  resqrexlemdec  10986  resqrexlemlo  10988  resqrexlemcalc1  10989  resqrexlemcalc2  10990  resqrexlemnm  10993  resqrexlemcvg  10994  resqrexlemoverl  10996  resqrexlemglsq  10997  resqrexlemga  10998  abs00ap  11037  absext  11038  absrele  11058  abstri  11079  abs3lem  11086  amgm2  11093  qdenre  11177  maxabsle  11179  maxabslemlub  11182  maxabslemval  11183  maxcl  11185  maxltsup  11193  bdtrilem  11213  bdtri  11214  xrbdtri  11250  mulcn2  11286  fsumabs  11439  cvgratnnlembern  11497  eirraplem  11750  ltoddhalfle  11863  divalglemnqt  11890  zssinfcl  11914  xblss2ps  13455  cnopnap  13645  ivthinclemlopn  13665  ivthinclemuopn  13667  limcimolemlt  13684  efltlemlt  13746  cosq23lt0  13805  cosordlem  13821  lgsdirprm  13986  2sqlem8  14010  qdencn  14316  trilpolemeq1  14329