Theorem readdcld 8049

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 7998	. 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 2164  (class class class)co 5918   RRcr 7871   + caddc 7875

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

This theorem is referenced by:  ltadd2  8438  leadd1  8449  le2add  8463  lt2add  8464  lesub2  8476  ltsub2  8478  gt0add  8592  reapadd1  8615  apadd1  8627  mulext1  8631  recexaplem2  8671  recp1lt1  8918  cju  8980  peano5nni  8985  peano2nn  8994  div4p1lem1div2  9236  peano2z  9353  difgtsumgt  9386  addlelt  9834  xaddf  9910  xaddval  9911  xleaddadd  9953  zltaddlt1le  10073  exbtwnzlemstep  10316  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnrelemcalc  10324  flqaddz  10366  btwnzge0  10369  2tnp1ge0ge0  10370  flhalf  10371  modqltm1p1mod  10447  expnbnd  10734  nn0opthlem2d  10792  remim  11004  remullem  11015  caucvgrelemcau  11124  caucvgre  11125  cvg1nlemcxze  11126  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniqlem  11138  resqrexlem1arp  11149  resqrexlemp1rp  11150  resqrexlemf1  11152  resqrexlemfp1  11153  resqrexlemover  11154  resqrexlemdec  11155  resqrexlemlo  11157  resqrexlemcalc1  11158  resqrexlemcalc2  11159  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  abs00ap  11206  absext  11207  absrele  11227  abstri  11248  abs3lem  11255  amgm2  11262  qdenre  11346  maxabsle  11348  maxabslemlub  11351  maxabslemval  11352  maxcl  11354  maxltsup  11362  bdtrilem  11382  bdtri  11383  xrbdtri  11419  mulcn2  11455  fsumabs  11608  cvgratnnlembern  11666  eirraplem  11920  ltoddhalfle  12034  divalglemnqt  12061  zssinfcl  12085  4sqlem12  12540  4sqlem15  12543  4sqlem16  12544  xblss2ps  14572  cnopnap  14765  maxcncf  14769  mincncf  14770  ivthinclemlopn  14790  ivthinclemuopn  14792  hoverb  14802  ivthdichlem  14805  limcimolemlt  14818  efltlemlt  14909  cosq23lt0  14968  cosordlem  14984  lgsdirprm  15150  gausslemma2dlem1a  15174  2sqlem8  15210  qdencn  15517  trilpolemeq1  15530