Theorem readdcld 8187

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 8136	. 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 2200  (class class class)co 6007   RRcr 8009   + caddc 8013

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

This theorem is referenced by:  ltadd2  8577  leadd1  8588  le2add  8602  lt2add  8603  lesub2  8615  ltsub2  8617  gt0add  8731  reapadd1  8754  apadd1  8766  mulext1  8770  recexaplem2  8810  recp1lt1  9057  cju  9119  peano5nni  9124  peano2nn  9133  div4p1lem1div2  9376  peano2z  9493  difgtsumgt  9527  eluzmn  9740  addlelt  9976  xaddf  10052  xaddval  10053  xleaddadd  10095  zltaddlt1le  10215  elincfzoext  10411  zssinfcl  10464  exbtwnzlemstep  10479  exbtwnz  10482  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnrelemcalc  10487  flqaddz  10529  btwnzge0  10532  2tnp1ge0ge0  10533  flhalf  10534  modqltm1p1mod  10610  expnbnd  10897  nn0opthlem2d  10955  ccatalpha  11161  remim  11386  remullem  11397  caucvgrelemcau  11506  caucvgre  11507  cvg1nlemcxze  11508  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniqlem  11520  resqrexlem1arp  11531  resqrexlemp1rp  11532  resqrexlemf1  11534  resqrexlemfp1  11535  resqrexlemover  11536  resqrexlemdec  11537  resqrexlemlo  11539  resqrexlemcalc1  11540  resqrexlemcalc2  11541  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  abs00ap  11588  absext  11589  absrele  11609  abstri  11630  abs3lem  11637  amgm2  11644  qdenre  11728  maxabsle  11730  maxabslemlub  11733  maxabslemval  11734  maxcl  11736  maxltsup  11744  bdtrilem  11765  bdtri  11766  xrbdtri  11802  mulcn2  11838  fsumabs  11991  cvgratnnlembern  12049  eirraplem  12303  ltoddhalfle  12419  divalglemnqt  12446  bitscmp  12484  4sqlem12  12940  4sqlem15  12943  4sqlem16  12944  2expltfac  12977  xblss2ps  15093  cnopnap  15300  maxcncf  15304  mincncf  15305  ivthinclemlopn  15325  ivthinclemuopn  15327  hoverb  15337  ivthdichlem  15340  limcimolemlt  15353  efltlemlt  15463  cosq23lt0  15522  cosordlem  15538  lgsdirprm  15728  gausslemma2dlem1a  15752  2sqlem8  15817  qdencn  16455  trilpolemeq1  16468