Theorem readdcld 7989

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

Syntax hints:   → wi 4   ∈ wcel 2148  (class class class)co 5877  ℝcr 7812   + caddc 7816

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

This theorem is referenced by:  ltadd2  8378  leadd1  8389  le2add  8403  lt2add  8404  lesub2  8416  ltsub2  8418  gt0add  8532  reapadd1  8555  apadd1  8567  mulext1  8571  recexaplem2  8611  recp1lt1  8858  cju  8920  peano5nni  8924  peano2nn  8933  div4p1lem1div2  9174  peano2z  9291  difgtsumgt  9324  addlelt  9770  xaddf  9846  xaddval  9847  xleaddadd  9889  zltaddlt1le  10009  exbtwnzlemstep  10250  exbtwnz  10253  rebtwn2zlemstep  10255  rebtwn2z  10257  qbtwnrelemcalc  10258  flqaddz  10299  btwnzge0  10302  2tnp1ge0ge0  10303  flhalf  10304  modqltm1p1mod  10378  expnbnd  10646  nn0opthlem2d  10703  remim  10871  remullem  10882  caucvgrelemcau  10991  caucvgre  10992  cvg1nlemcxze  10993  cvg1nlemcau  10995  cvg1nlemres  10996  recvguniqlem  11005  resqrexlem1arp  11016  resqrexlemp1rp  11017  resqrexlemf1  11019  resqrexlemfp1  11020  resqrexlemover  11021  resqrexlemdec  11022  resqrexlemlo  11024  resqrexlemcalc1  11025  resqrexlemcalc2  11026  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemoverl  11032  resqrexlemglsq  11033  resqrexlemga  11034  abs00ap  11073  absext  11074  absrele  11094  abstri  11115  abs3lem  11122  amgm2  11129  qdenre  11213  maxabsle  11215  maxabslemlub  11218  maxabslemval  11219  maxcl  11221  maxltsup  11229  bdtrilem  11249  bdtri  11250  xrbdtri  11286  mulcn2  11322  fsumabs  11475  cvgratnnlembern  11533  eirraplem  11786  ltoddhalfle  11900  divalglemnqt  11927  zssinfcl  11951  xblss2ps  13989  cnopnap  14179  ivthinclemlopn  14199  ivthinclemuopn  14201  limcimolemlt  14218  efltlemlt  14280  cosq23lt0  14339  cosordlem  14355  lgsdirprm  14520  2sqlem8  14555  qdencn  14860  trilpolemeq1  14873