Theorem readdcld 7907

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

Syntax hints:   → wi 4   ∈ wcel 2128  (class class class)co 5824  ℝcr 7731   + caddc 7735

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

This theorem is referenced by:  ltadd2  8294  leadd1  8305  le2add  8319  lt2add  8320  lesub2  8332  ltsub2  8334  gt0add  8448  reapadd1  8471  apadd1  8483  mulext1  8487  recexaplem2  8526  recp1lt1  8770  cju  8832  peano5nni  8836  peano2nn  8845  div4p1lem1div2  9086  peano2z  9203  addlelt  9675  xaddf  9748  xaddval  9749  xleaddadd  9791  zltaddlt1le  9911  exbtwnzlemstep  10147  exbtwnz  10150  rebtwn2zlemstep  10152  rebtwn2z  10154  qbtwnrelemcalc  10155  flqaddz  10196  btwnzge0  10199  2tnp1ge0ge0  10200  flhalf  10201  modqltm1p1mod  10275  expnbnd  10541  nn0opthlem2d  10595  remim  10760  remullem  10771  caucvgrelemcau  10880  caucvgre  10881  cvg1nlemcxze  10882  cvg1nlemcau  10884  cvg1nlemres  10885  recvguniqlem  10894  resqrexlem1arp  10905  resqrexlemp1rp  10906  resqrexlemf1  10908  resqrexlemfp1  10909  resqrexlemover  10910  resqrexlemdec  10911  resqrexlemlo  10913  resqrexlemcalc1  10914  resqrexlemcalc2  10915  resqrexlemnm  10918  resqrexlemcvg  10919  resqrexlemoverl  10921  resqrexlemglsq  10922  resqrexlemga  10923  abs00ap  10962  absext  10963  absrele  10983  abstri  11004  abs3lem  11011  amgm2  11018  qdenre  11102  maxabsle  11104  maxabslemlub  11107  maxabslemval  11108  maxcl  11110  maxltsup  11118  bdtrilem  11138  bdtri  11139  xrbdtri  11173  mulcn2  11209  fsumabs  11362  cvgratnnlembern  11420  eirraplem  11673  ltoddhalfle  11783  divalglemnqt  11810  zssinfcl  11834  xblss2ps  12804  cnopnap  12994  ivthinclemlopn  13014  ivthinclemuopn  13016  limcimolemlt  13033  efltlemlt  13095  cosq23lt0  13154  cosordlem  13170  qdencn  13598  trilpolemeq1  13611