Theorem readdcld 8109

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 8058	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2177  (class class class)co 5951  ℝcr 7931   + caddc 7935

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

This theorem is referenced by:  ltadd2  8499  leadd1  8510  le2add  8524  lt2add  8525  lesub2  8537  ltsub2  8539  gt0add  8653  reapadd1  8676  apadd1  8688  mulext1  8692  recexaplem2  8732  recp1lt1  8979  cju  9041  peano5nni  9046  peano2nn  9055  div4p1lem1div2  9298  peano2z  9415  difgtsumgt  9449  addlelt  9897  xaddf  9973  xaddval  9974  xleaddadd  10016  zltaddlt1le  10136  elincfzoext  10329  zssinfcl  10382  exbtwnzlemstep  10397  exbtwnz  10400  rebtwn2zlemstep  10402  rebtwn2z  10404  qbtwnrelemcalc  10405  flqaddz  10447  btwnzge0  10450  2tnp1ge0ge0  10451  flhalf  10452  modqltm1p1mod  10528  expnbnd  10815  nn0opthlem2d  10873  remim  11215  remullem  11226  caucvgrelemcau  11335  caucvgre  11336  cvg1nlemcxze  11337  cvg1nlemcau  11339  cvg1nlemres  11340  recvguniqlem  11349  resqrexlem1arp  11360  resqrexlemp1rp  11361  resqrexlemf1  11363  resqrexlemfp1  11364  resqrexlemover  11365  resqrexlemdec  11366  resqrexlemlo  11368  resqrexlemcalc1  11369  resqrexlemcalc2  11370  resqrexlemnm  11373  resqrexlemcvg  11374  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemga  11378  abs00ap  11417  absext  11418  absrele  11438  abstri  11459  abs3lem  11466  amgm2  11473  qdenre  11557  maxabsle  11559  maxabslemlub  11562  maxabslemval  11563  maxcl  11565  maxltsup  11573  bdtrilem  11594  bdtri  11595  xrbdtri  11631  mulcn2  11667  fsumabs  11820  cvgratnnlembern  11878  eirraplem  12132  ltoddhalfle  12248  divalglemnqt  12275  bitscmp  12313  4sqlem12  12769  4sqlem15  12772  4sqlem16  12773  2expltfac  12806  xblss2ps  14920  cnopnap  15127  maxcncf  15131  mincncf  15132  ivthinclemlopn  15152  ivthinclemuopn  15154  hoverb  15164  ivthdichlem  15167  limcimolemlt  15180  efltlemlt  15290  cosq23lt0  15349  cosordlem  15365  lgsdirprm  15555  gausslemma2dlem1a  15579  2sqlem8  15644  qdencn  16040  trilpolemeq1  16053