Theorem readdcld 8308

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

Syntax hints:   → wi 4   ∈ wcel 2205  (class class class)co 6052  ℝcr 8131   + caddc 8135

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

This theorem is referenced by:  ltadd2  8698  leadd1  8709  le2add  8723  lt2add  8724  lesub2  8736  ltsub2  8738  gt0add  8852  reapadd1  8875  apadd1  8887  mulext1  8891  recexaplem2  8931  recp1lt1  9178  cju  9240  peano5nni  9245  peano2nn  9254  div4p1lem1div2  9497  peano2z  9618  difgtsumgt  9652  eluzmn  9866  addlelt  10107  xaddf  10183  xaddval  10184  xleaddadd  10226  lincmble  10343  zltaddlt1le  10347  elincfzoext  10545  zssinfcl  10599  exbtwnzlemstep  10614  exbtwnz  10617  rebtwn2zlemstep  10619  rebtwn2z  10621  qbtwnrelemcalc  10622  flqaddz  10664  btwnzge0  10667  2tnp1ge0ge0  10668  flhalf  10669  modqltm1p1mod  10745  expnbnd  11033  nn0opthlem2d  11091  ccatalpha  11309  remim  11553  remullem  11564  caucvgrelemcau  11673  caucvgre  11674  cvg1nlemcxze  11675  cvg1nlemcau  11677  cvg1nlemres  11678  recvguniqlem  11687  resqrexlem1arp  11698  resqrexlemp1rp  11699  resqrexlemf1  11701  resqrexlemfp1  11702  resqrexlemover  11703  resqrexlemdec  11704  resqrexlemlo  11706  resqrexlemcalc1  11707  resqrexlemcalc2  11708  resqrexlemnm  11711  resqrexlemcvg  11712  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemga  11716  abs00ap  11755  absext  11756  absrele  11776  abstri  11797  abs3lem  11804  amgm2  11811  qdenre  11895  maxabsle  11897  maxabslemlub  11900  maxabslemval  11901  maxcl  11903  maxltsup  11911  bdtrilem  11932  bdtri  11933  xrbdtri  11969  mulcn2  12005  fsumabs  12159  cvgratnnlembern  12217  eirraplem  12471  ltoddhalfle  12587  divalglemnqt  12614  bitscmp  12652  4sqlem12  13108  4sqlem15  13111  4sqlem16  13112  2expltfac  13145  xblss2ps  15318  cnopnap  15525  maxcncf  15529  mincncf  15530  ivthinclemlopn  15550  ivthinclemuopn  15552  hoverb  15562  ivthdichlem  15565  limcimolemlt  15578  efltlemlt  15688  cosq23lt0  15747  cosordlem  15763  pellexlem2  15895  lgsdirprm  15956  gausslemma2dlem1a  15980  2sqlem8  16045  qdencn  16856  repiecelem  16858  trilpolemeq1  16873