Theorem readdcld 7517

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

Syntax hints:   → wi 4   ∈ wcel 1438  (class class class)co 5652  ℝcr 7349   + caddc 7353

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

This theorem is referenced by:  ltadd2  7897  leadd1  7908  le2add  7922  lt2add  7923  lesub2  7935  ltsub2  7937  gt0add  8050  reapadd1  8073  apadd1  8085  mulext1  8089  recexaplem2  8121  recp1lt1  8360  cju  8421  peano5nni  8425  peano2nn  8434  div4p1lem1div2  8669  peano2z  8786  addlelt  9239  zltaddlt1le  9423  exbtwnzlemstep  9659  exbtwnz  9662  rebtwn2zlemstep  9664  rebtwn2z  9666  qbtwnrelemcalc  9667  flqaddz  9704  btwnzge0  9707  2tnp1ge0ge0  9708  flhalf  9709  modqltm1p1mod  9783  expnbnd  10077  nn0opthlem2d  10129  remim  10294  remullem  10305  caucvgrelemcau  10413  caucvgre  10414  cvg1nlemcxze  10415  cvg1nlemcau  10417  cvg1nlemres  10418  recvguniqlem  10427  resqrexlem1arp  10438  resqrexlemp1rp  10439  resqrexlemf1  10441  resqrexlemfp1  10442  resqrexlemover  10443  resqrexlemdec  10444  resqrexlemlo  10446  resqrexlemcalc1  10447  resqrexlemcalc2  10448  resqrexlemnm  10451  resqrexlemcvg  10452  resqrexlemoverl  10454  resqrexlemglsq  10455  resqrexlemga  10456  abs00ap  10495  absext  10496  absrele  10516  abstri  10537  abs3lem  10544  amgm2  10551  qdenre  10635  maxabsle  10637  maxabslemlub  10640  maxabslemval  10641  maxcl  10643  maxltsup  10651  mulcn2  10701  fsumabs  10859  cvgratnnlembern  10917  eirraplem  11064  ltoddhalfle  11171  divalglemnqt  11198  zssinfcl  11222  qdencn  11915