Theorem readdcld 8349

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

Syntax hints:   → wi 4   ∈ wcel 2209  (class class class)co 6079  ℝcr 8172   + caddc 8176

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

This theorem is referenced by:  ltadd2  8741  leadd1  8752  le2add  8766  lt2add  8767  lesub2  8779  ltsub2  8781  gt0add  8895  reapadd1  8918  apadd1  8930  mulext1  8934  recexaplem2  8974  recp1lt1  9223  cju  9285  peano5nni  9290  peano2nn  9299  div4p1lem1div2  9542  peano2z  9663  difgtsumgt  9697  eluzmn  9911  addlelt  10152  xaddf  10229  xaddval  10230  xleaddadd  10272  lincmble  10389  zltaddlt1le  10393  elincfzoext  10594  zssinfcl  10648  exbtwnzlemstep  10665  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnrelemcalc  10673  flqaddz  10715  btwnzge0  10718  2tnp1ge0ge0  10719  flhalf  10720  modqltm1p1mod  10796  expnbnd  11084  nn0opthlem2d  11142  ccatalpha  11364  remim  11608  remullem  11619  sq01  11643  caucvgrelemcau  11729  caucvgre  11730  cvg1nlemcxze  11731  cvg1nlemcau  11733  cvg1nlemres  11734  recvguniqlem  11743  resqrexlem1arp  11754  resqrexlemp1rp  11755  resqrexlemf1  11757  resqrexlemfp1  11758  resqrexlemover  11759  resqrexlemdec  11760  resqrexlemlo  11762  resqrexlemcalc1  11763  resqrexlemcalc2  11764  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemga  11772  abs00ap  11811  absext  11812  absrele  11832  abstri  11853  abs3lem  11860  amgm2  11867  qdenre  11951  maxabsle  11953  maxabslemlub  11956  maxabslemval  11957  maxcl  11959  maxltsup  11967  bdtrilem  11988  bdtri  11989  xrbdtri  12025  mulcn2  12061  fsumabs  12215  cvgratnnlembern  12273  eirraplem  12527  ltoddhalfle  12643  divalglemnqt  12670  bitscmp  12708  4sqlem12  13164  4sqlem15  13167  4sqlem16  13168  2expltfac  13201  ballotfilemsgt1  13237  ballotfilemsel1i  13239  xblss2ps  15488  cnopnap  15695  maxcncf  15699  mincncf  15700  ivthinclemlopn  15720  ivthinclemuopn  15722  hoverb  15732  ivthdichlem  15735  limcimolemlt  15748  efltlemlt  15858  cosq23lt0  15917  cosordlem  15933  pellexlem2  16075  lgsdirprm  16136  gausslemma2dlem1a  16160  2sqlem8  16225  qdencn  17046  repiecelem  17048  trilpolemeq1  17063