Theorem readdcld 7986

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 7936	. 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 5874   RRcr 7809   + caddc 7813

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

This theorem is referenced by:  ltadd2  8375  leadd1  8386  le2add  8400  lt2add  8401  lesub2  8413  ltsub2  8415  gt0add  8529  reapadd1  8552  apadd1  8564  mulext1  8568  recexaplem2  8608  recp1lt1  8855  cju  8917  peano5nni  8921  peano2nn  8930  div4p1lem1div2  9171  peano2z  9288  difgtsumgt  9321  addlelt  9767  xaddf  9843  xaddval  9844  xleaddadd  9886  zltaddlt1le  10006  exbtwnzlemstep  10247  exbtwnz  10250  rebtwn2zlemstep  10252  rebtwn2z  10254  qbtwnrelemcalc  10255  flqaddz  10296  btwnzge0  10299  2tnp1ge0ge0  10300  flhalf  10301  modqltm1p1mod  10375  expnbnd  10643  nn0opthlem2d  10700  remim  10868  remullem  10879  caucvgrelemcau  10988  caucvgre  10989  cvg1nlemcxze  10990  cvg1nlemcau  10992  cvg1nlemres  10993  recvguniqlem  11002  resqrexlem1arp  11013  resqrexlemp1rp  11014  resqrexlemf1  11016  resqrexlemfp1  11017  resqrexlemover  11018  resqrexlemdec  11019  resqrexlemlo  11021  resqrexlemcalc1  11022  resqrexlemcalc2  11023  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  abs00ap  11070  absext  11071  absrele  11091  abstri  11112  abs3lem  11119  amgm2  11126  qdenre  11210  maxabsle  11212  maxabslemlub  11215  maxabslemval  11216  maxcl  11218  maxltsup  11226  bdtrilem  11246  bdtri  11247  xrbdtri  11283  mulcn2  11319  fsumabs  11472  cvgratnnlembern  11530  eirraplem  11783  ltoddhalfle  11897  divalglemnqt  11924  zssinfcl  11948  xblss2ps  13874  cnopnap  14064  ivthinclemlopn  14084  ivthinclemuopn  14086  limcimolemlt  14103  efltlemlt  14165  cosq23lt0  14224  cosordlem  14240  lgsdirprm  14405  2sqlem8  14440  qdencn  14745  trilpolemeq1  14758