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  caucvgrelemcau  11693  caucvgre  11694  cvg1nlemcxze  11695  cvg1nlemcau  11697  cvg1nlemres  11698  recvguniqlem  11707  resqrexlem1arp  11718  resqrexlemp1rp  11719  resqrexlemf1  11721  resqrexlemfp1  11722  resqrexlemover  11723  resqrexlemdec  11724  resqrexlemlo  11726  resqrexlemcalc1  11727  resqrexlemcalc2  11728  resqrexlemnm  11731  resqrexlemcvg  11732  resqrexlemoverl  11734  resqrexlemglsq  11735  resqrexlemga  11736  abs00ap  11775  absext  11776  absrele  11796  abstri  11817  abs3lem  11824  amgm2  11831  qdenre  11915  maxabsle  11917  maxabslemlub  11920  maxabslemval  11921  maxcl  11923  maxltsup  11931  bdtrilem  11952  bdtri  11953  xrbdtri  11989  mulcn2  12025  fsumabs  12179  cvgratnnlembern  12237  eirraplem  12491  ltoddhalfle  12607  divalglemnqt  12634  bitscmp  12672  4sqlem12  13128  4sqlem15  13131  4sqlem16  13132  2expltfac  13165  ballotfilemsgt1  13201  ballotfilemsel1i  13203  xblss2ps  15398  cnopnap  15605  maxcncf  15609  mincncf  15610  ivthinclemlopn  15630  ivthinclemuopn  15632  hoverb  15642  ivthdichlem  15645  limcimolemlt  15658  efltlemlt  15768  cosq23lt0  15827  cosordlem  15843  pellexlem2  15975  lgsdirprm  16036  gausslemma2dlem1a  16060  2sqlem8  16125  qdencn  16946  repiecelem  16948  trilpolemeq1  16963