Theorem readdcld 7928

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

Syntax hints:   → wi 4   ∈ wcel 2136  (class class class)co 5842  ℝcr 7752   + caddc 7756

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

This theorem is referenced by:  ltadd2  8317  leadd1  8328  le2add  8342  lt2add  8343  lesub2  8355  ltsub2  8357  gt0add  8471  reapadd1  8494  apadd1  8506  mulext1  8510  recexaplem2  8549  recp1lt1  8794  cju  8856  peano5nni  8860  peano2nn  8869  div4p1lem1div2  9110  peano2z  9227  difgtsumgt  9260  addlelt  9704  xaddf  9780  xaddval  9781  xleaddadd  9823  zltaddlt1le  9943  exbtwnzlemstep  10183  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnrelemcalc  10191  flqaddz  10232  btwnzge0  10235  2tnp1ge0ge0  10236  flhalf  10237  modqltm1p1mod  10311  expnbnd  10578  nn0opthlem2d  10634  remim  10802  remullem  10813  caucvgrelemcau  10922  caucvgre  10923  cvg1nlemcxze  10924  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniqlem  10936  resqrexlem1arp  10947  resqrexlemp1rp  10948  resqrexlemf1  10950  resqrexlemfp1  10951  resqrexlemover  10952  resqrexlemdec  10953  resqrexlemlo  10955  resqrexlemcalc1  10956  resqrexlemcalc2  10957  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  abs00ap  11004  absext  11005  absrele  11025  abstri  11046  abs3lem  11053  amgm2  11060  qdenre  11144  maxabsle  11146  maxabslemlub  11149  maxabslemval  11150  maxcl  11152  maxltsup  11160  bdtrilem  11180  bdtri  11181  xrbdtri  11217  mulcn2  11253  fsumabs  11406  cvgratnnlembern  11464  eirraplem  11717  ltoddhalfle  11830  divalglemnqt  11857  zssinfcl  11881  xblss2ps  13044  cnopnap  13234  ivthinclemlopn  13254  ivthinclemuopn  13256  limcimolemlt  13273  efltlemlt  13335  cosq23lt0  13394  cosordlem  13410  lgsdirprm  13575  2sqlem8  13599  qdencn  13906  trilpolemeq1  13919