Theorem readdcld 7788

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

Syntax hints:   → wi 4   ∈ wcel 1480  (class class class)co 5767  ℝcr 7612   + caddc 7616

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

This theorem is referenced by:  ltadd2  8174  leadd1  8185  le2add  8199  lt2add  8200  lesub2  8212  ltsub2  8214  gt0add  8328  reapadd1  8351  apadd1  8363  mulext1  8367  recexaplem2  8406  recp1lt1  8650  cju  8712  peano5nni  8716  peano2nn  8725  div4p1lem1div2  8966  peano2z  9083  addlelt  9548  xaddf  9620  xaddval  9621  xleaddadd  9663  zltaddlt1le  9782  exbtwnzlemstep  10018  exbtwnz  10021  rebtwn2zlemstep  10023  rebtwn2z  10025  qbtwnrelemcalc  10026  flqaddz  10063  btwnzge0  10066  2tnp1ge0ge0  10067  flhalf  10068  modqltm1p1mod  10142  expnbnd  10408  nn0opthlem2d  10460  remim  10625  remullem  10636  caucvgrelemcau  10745  caucvgre  10746  cvg1nlemcxze  10747  cvg1nlemcau  10749  cvg1nlemres  10750  recvguniqlem  10759  resqrexlem1arp  10770  resqrexlemp1rp  10771  resqrexlemf1  10773  resqrexlemfp1  10774  resqrexlemover  10775  resqrexlemdec  10776  resqrexlemlo  10778  resqrexlemcalc1  10779  resqrexlemcalc2  10780  resqrexlemnm  10783  resqrexlemcvg  10784  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemga  10788  abs00ap  10827  absext  10828  absrele  10848  abstri  10869  abs3lem  10876  amgm2  10883  qdenre  10967  maxabsle  10969  maxabslemlub  10972  maxabslemval  10973  maxcl  10975  maxltsup  10983  bdtrilem  11003  bdtri  11004  xrbdtri  11038  mulcn2  11074  fsumabs  11227  cvgratnnlembern  11285  eirraplem  11472  ltoddhalfle  11579  divalglemnqt  11606  zssinfcl  11630  xblss2ps  12562  cnopnap  12752  ivthinclemlopn  12772  ivthinclemuopn  12774  limcimolemlt  12791  cosq23lt0  12903  cosordlem  12919  qdencn  13211  trilpolemeq1  13222