Theorem readdcld 8319

Description: Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
readdcld.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
readdcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcld

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		readdcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		readdcl 8269	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2205  (class class class)co 6058  ℝcr 8142   + caddc 8146

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

This theorem is referenced by:  ltadd2  8711  leadd1  8722  le2add  8736  lt2add  8737  lesub2  8749  ltsub2  8751  gt0add  8865  reapadd1  8888  apadd1  8900  mulext1  8904  recexaplem2  8944  recp1lt1  9193  cju  9255  peano5nni  9260  peano2nn  9269  div4p1lem1div2  9512  peano2z  9633  difgtsumgt  9667  eluzmn  9881  addlelt  10122  xaddf  10199  xaddval  10200  xleaddadd  10242  lincmble  10359  zltaddlt1le  10363  elincfzoext  10563  zssinfcl  10617  exbtwnzlemstep  10634  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnrelemcalc  10642  flqaddz  10684  btwnzge0  10687  2tnp1ge0ge0  10688  flhalf  10689  modqltm1p1mod  10765  expnbnd  11053  nn0opthlem2d  11111  ccatalpha  11329  remim  11573  remullem  11584  sq01  11608  caucvgrelemcau  11694  caucvgre  11695  cvg1nlemcxze  11696  cvg1nlemcau  11698  cvg1nlemres  11699  recvguniqlem  11708  resqrexlem1arp  11719  resqrexlemp1rp  11720  resqrexlemf1  11722  resqrexlemfp1  11723  resqrexlemover  11724  resqrexlemdec  11725  resqrexlemlo  11727  resqrexlemcalc1  11728  resqrexlemcalc2  11729  resqrexlemnm  11732  resqrexlemcvg  11733  resqrexlemoverl  11735  resqrexlemglsq  11736  resqrexlemga  11737  abs00ap  11776  absext  11777  absrele  11797  abstri  11818  abs3lem  11825  amgm2  11832  qdenre  11916  maxabsle  11918  maxabslemlub  11921  maxabslemval  11922  maxcl  11924  maxltsup  11932  bdtrilem  11953  bdtri  11954  xrbdtri  11990  mulcn2  12026  fsumabs  12180  cvgratnnlembern  12238  eirraplem  12492  ltoddhalfle  12608  divalglemnqt  12635  bitscmp  12673  4sqlem12  13129  4sqlem15  13132  4sqlem16  13133  2expltfac  13166  ballotfilemsgt1  13202  ballotfilemsel1i  13204  xblss2ps  15399  cnopnap  15606  maxcncf  15610  mincncf  15611  ivthinclemlopn  15631  ivthinclemuopn  15633  hoverb  15643  ivthdichlem  15646  limcimolemlt  15659  efltlemlt  15769  cosq23lt0  15828  cosordlem  15844  pellexlem2  15976  lgsdirprm  16037  gausslemma2dlem1a  16061  2sqlem8  16126  qdencn  16947  repiecelem  16949  trilpolemeq1  16964