Theorem readdcld 7886

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

Syntax hints:   -> wi 4   e. wcel 2125  (class class class)co 5814   RRcr 7710   + caddc 7714

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

This theorem is referenced by:  ltadd2  8273  leadd1  8284  le2add  8298  lt2add  8299  lesub2  8311  ltsub2  8313  gt0add  8427  reapadd1  8450  apadd1  8462  mulext1  8466  recexaplem2  8505  recp1lt1  8749  cju  8811  peano5nni  8815  peano2nn  8824  div4p1lem1div2  9065  peano2z  9182  addlelt  9653  xaddf  9726  xaddval  9727  xleaddadd  9769  zltaddlt1le  9889  exbtwnzlemstep  10125  exbtwnz  10128  rebtwn2zlemstep  10130  rebtwn2z  10132  qbtwnrelemcalc  10133  flqaddz  10174  btwnzge0  10177  2tnp1ge0ge0  10178  flhalf  10179  modqltm1p1mod  10253  expnbnd  10519  nn0opthlem2d  10572  remim  10737  remullem  10748  caucvgrelemcau  10857  caucvgre  10858  cvg1nlemcxze  10859  cvg1nlemcau  10861  cvg1nlemres  10862  recvguniqlem  10871  resqrexlem1arp  10882  resqrexlemp1rp  10883  resqrexlemf1  10885  resqrexlemfp1  10886  resqrexlemover  10887  resqrexlemdec  10888  resqrexlemlo  10890  resqrexlemcalc1  10891  resqrexlemcalc2  10892  resqrexlemnm  10895  resqrexlemcvg  10896  resqrexlemoverl  10898  resqrexlemglsq  10899  resqrexlemga  10900  abs00ap  10939  absext  10940  absrele  10960  abstri  10981  abs3lem  10988  amgm2  10995  qdenre  11079  maxabsle  11081  maxabslemlub  11084  maxabslemval  11085  maxcl  11087  maxltsup  11095  bdtrilem  11115  bdtri  11116  xrbdtri  11150  mulcn2  11186  fsumabs  11339  cvgratnnlembern  11397  eirraplem  11650  ltoddhalfle  11757  divalglemnqt  11784  zssinfcl  11808  xblss2ps  12751  cnopnap  12941  ivthinclemlopn  12961  ivthinclemuopn  12963  limcimolemlt  12980  efltlemlt  13042  cosq23lt0  13101  cosordlem  13117  qdencn  13547  trilpolemeq1  13560