Theorem readdcld 7949

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

Syntax hints:   → wi 4   ∈ wcel 2141  (class class class)co 5853  ℝcr 7773   + caddc 7777

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

This theorem is referenced by:  ltadd2  8338  leadd1  8349  le2add  8363  lt2add  8364  lesub2  8376  ltsub2  8378  gt0add  8492  reapadd1  8515  apadd1  8527  mulext1  8531  recexaplem2  8570  recp1lt1  8815  cju  8877  peano5nni  8881  peano2nn  8890  div4p1lem1div2  9131  peano2z  9248  difgtsumgt  9281  addlelt  9725  xaddf  9801  xaddval  9802  xleaddadd  9844  zltaddlt1le  9964  exbtwnzlemstep  10204  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnrelemcalc  10212  flqaddz  10253  btwnzge0  10256  2tnp1ge0ge0  10257  flhalf  10258  modqltm1p1mod  10332  expnbnd  10599  nn0opthlem2d  10655  remim  10824  remullem  10835  caucvgrelemcau  10944  caucvgre  10945  cvg1nlemcxze  10946  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniqlem  10958  resqrexlem1arp  10969  resqrexlemp1rp  10970  resqrexlemf1  10972  resqrexlemfp1  10973  resqrexlemover  10974  resqrexlemdec  10975  resqrexlemlo  10977  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemnm  10982  resqrexlemcvg  10983  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemga  10987  abs00ap  11026  absext  11027  absrele  11047  abstri  11068  abs3lem  11075  amgm2  11082  qdenre  11166  maxabsle  11168  maxabslemlub  11171  maxabslemval  11172  maxcl  11174  maxltsup  11182  bdtrilem  11202  bdtri  11203  xrbdtri  11239  mulcn2  11275  fsumabs  11428  cvgratnnlembern  11486  eirraplem  11739  ltoddhalfle  11852  divalglemnqt  11879  zssinfcl  11903  xblss2ps  13198  cnopnap  13388  ivthinclemlopn  13408  ivthinclemuopn  13410  limcimolemlt  13427  efltlemlt  13489  cosq23lt0  13548  cosordlem  13564  lgsdirprm  13729  2sqlem8  13753  qdencn  14059  trilpolemeq1  14072