Theorem readdcld 8184

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6007  ℝcr 8006   + caddc 8010

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

This theorem is referenced by:  ltadd2  8574  leadd1  8585  le2add  8599  lt2add  8600  lesub2  8612  ltsub2  8614  gt0add  8728  reapadd1  8751  apadd1  8763  mulext1  8767  recexaplem2  8807  recp1lt1  9054  cju  9116  peano5nni  9121  peano2nn  9130  div4p1lem1div2  9373  peano2z  9490  difgtsumgt  9524  addlelt  9972  xaddf  10048  xaddval  10049  xleaddadd  10091  zltaddlt1le  10211  elincfzoext  10407  zssinfcl  10460  exbtwnzlemstep  10475  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnrelemcalc  10483  flqaddz  10525  btwnzge0  10528  2tnp1ge0ge0  10529  flhalf  10530  modqltm1p1mod  10606  expnbnd  10893  nn0opthlem2d  10951  remim  11379  remullem  11390  caucvgrelemcau  11499  caucvgre  11500  cvg1nlemcxze  11501  cvg1nlemcau  11503  cvg1nlemres  11504  recvguniqlem  11513  resqrexlem1arp  11524  resqrexlemp1rp  11525  resqrexlemf1  11527  resqrexlemfp1  11528  resqrexlemover  11529  resqrexlemdec  11530  resqrexlemlo  11532  resqrexlemcalc1  11533  resqrexlemcalc2  11534  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemga  11542  abs00ap  11581  absext  11582  absrele  11602  abstri  11623  abs3lem  11630  amgm2  11637  qdenre  11721  maxabsle  11723  maxabslemlub  11726  maxabslemval  11727  maxcl  11729  maxltsup  11737  bdtrilem  11758  bdtri  11759  xrbdtri  11795  mulcn2  11831  fsumabs  11984  cvgratnnlembern  12042  eirraplem  12296  ltoddhalfle  12412  divalglemnqt  12439  bitscmp  12477  4sqlem12  12933  4sqlem15  12936  4sqlem16  12937  2expltfac  12970  xblss2ps  15086  cnopnap  15293  maxcncf  15297  mincncf  15298  ivthinclemlopn  15318  ivthinclemuopn  15320  hoverb  15330  ivthdichlem  15333  limcimolemlt  15346  efltlemlt  15456  cosq23lt0  15515  cosordlem  15531  lgsdirprm  15721  gausslemma2dlem1a  15745  2sqlem8  15810  qdencn  16425  trilpolemeq1  16438