Theorem readdcld 8209

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 8158	. 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 2202  (class class class)co 6018   RRcr 8031   + caddc 8035

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

This theorem is referenced by:  ltadd2  8599  leadd1  8610  le2add  8624  lt2add  8625  lesub2  8637  ltsub2  8639  gt0add  8753  reapadd1  8776  apadd1  8788  mulext1  8792  recexaplem2  8832  recp1lt1  9079  cju  9141  peano5nni  9146  peano2nn  9155  div4p1lem1div2  9398  peano2z  9515  difgtsumgt  9549  eluzmn  9762  addlelt  10003  xaddf  10079  xaddval  10080  xleaddadd  10122  zltaddlt1le  10242  elincfzoext  10439  zssinfcl  10493  exbtwnzlemstep  10508  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnrelemcalc  10516  flqaddz  10558  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  modqltm1p1mod  10639  expnbnd  10926  nn0opthlem2d  10984  ccatalpha  11194  remim  11425  remullem  11436  caucvgrelemcau  11545  caucvgre  11546  cvg1nlemcxze  11547  cvg1nlemcau  11549  cvg1nlemres  11550  recvguniqlem  11559  resqrexlem1arp  11570  resqrexlemp1rp  11571  resqrexlemf1  11573  resqrexlemfp1  11574  resqrexlemover  11575  resqrexlemdec  11576  resqrexlemlo  11578  resqrexlemcalc1  11579  resqrexlemcalc2  11580  resqrexlemnm  11583  resqrexlemcvg  11584  resqrexlemoverl  11586  resqrexlemglsq  11587  resqrexlemga  11588  abs00ap  11627  absext  11628  absrele  11648  abstri  11669  abs3lem  11676  amgm2  11683  qdenre  11767  maxabsle  11769  maxabslemlub  11772  maxabslemval  11773  maxcl  11775  maxltsup  11783  bdtrilem  11804  bdtri  11805  xrbdtri  11841  mulcn2  11877  fsumabs  12031  cvgratnnlembern  12089  eirraplem  12343  ltoddhalfle  12459  divalglemnqt  12486  bitscmp  12524  4sqlem12  12980  4sqlem15  12983  4sqlem16  12984  2expltfac  13017  xblss2ps  15134  cnopnap  15341  maxcncf  15345  mincncf  15346  ivthinclemlopn  15366  ivthinclemuopn  15368  hoverb  15378  ivthdichlem  15381  limcimolemlt  15394  efltlemlt  15504  cosq23lt0  15563  cosordlem  15579  lgsdirprm  15769  gausslemma2dlem1a  15793  2sqlem8  15858  qdencn  16657  trilpolemeq1  16670