Theorem readdcld 8144

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

Syntax hints:   → wi 4   ∈ wcel 2180  (class class class)co 5974  ℝcr 7966   + caddc 7970

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

This theorem is referenced by:  ltadd2  8534  leadd1  8545  le2add  8559  lt2add  8560  lesub2  8572  ltsub2  8574  gt0add  8688  reapadd1  8711  apadd1  8723  mulext1  8727  recexaplem2  8767  recp1lt1  9014  cju  9076  peano5nni  9081  peano2nn  9090  div4p1lem1div2  9333  peano2z  9450  difgtsumgt  9484  addlelt  9932  xaddf  10008  xaddval  10009  xleaddadd  10051  zltaddlt1le  10171  elincfzoext  10366  zssinfcl  10419  exbtwnzlemstep  10434  exbtwnz  10437  rebtwn2zlemstep  10439  rebtwn2z  10441  qbtwnrelemcalc  10442  flqaddz  10484  btwnzge0  10487  2tnp1ge0ge0  10488  flhalf  10489  modqltm1p1mod  10565  expnbnd  10852  nn0opthlem2d  10910  remim  11337  remullem  11348  caucvgrelemcau  11457  caucvgre  11458  cvg1nlemcxze  11459  cvg1nlemcau  11461  cvg1nlemres  11462  recvguniqlem  11471  resqrexlem1arp  11482  resqrexlemp1rp  11483  resqrexlemf1  11485  resqrexlemfp1  11486  resqrexlemover  11487  resqrexlemdec  11488  resqrexlemlo  11490  resqrexlemcalc1  11491  resqrexlemcalc2  11492  resqrexlemnm  11495  resqrexlemcvg  11496  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemga  11500  abs00ap  11539  absext  11540  absrele  11560  abstri  11581  abs3lem  11588  amgm2  11595  qdenre  11679  maxabsle  11681  maxabslemlub  11684  maxabslemval  11685  maxcl  11687  maxltsup  11695  bdtrilem  11716  bdtri  11717  xrbdtri  11753  mulcn2  11789  fsumabs  11942  cvgratnnlembern  12000  eirraplem  12254  ltoddhalfle  12370  divalglemnqt  12397  bitscmp  12435  4sqlem12  12891  4sqlem15  12894  4sqlem16  12895  2expltfac  12928  xblss2ps  15043  cnopnap  15250  maxcncf  15254  mincncf  15255  ivthinclemlopn  15275  ivthinclemuopn  15277  hoverb  15287  ivthdichlem  15290  limcimolemlt  15303  efltlemlt  15413  cosq23lt0  15472  cosordlem  15488  lgsdirprm  15678  gausslemma2dlem1a  15702  2sqlem8  15767  qdencn  16306  trilpolemeq1  16319