Theorem readdcld 8209

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

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031   + caddc 8035

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

This theorem is referenced by:  ltadd2  8599  leadd1  8610  le2add  8624  lt2add  8625  lesub2  8637  ltsub2  8639  gt0add  8753  reapadd1  8776  apadd1  8788  mulext1  8792  recexaplem2  8832  recp1lt1  9079  cju  9141  peano5nni  9146  peano2nn  9155  div4p1lem1div2  9398  peano2z  9515  difgtsumgt  9549  eluzmn  9762  addlelt  10003  xaddf  10079  xaddval  10080  xleaddadd  10122  zltaddlt1le  10242  elincfzoext  10439  zssinfcl  10493  exbtwnzlemstep  10508  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnrelemcalc  10516  flqaddz  10558  btwnzge0  10561  2tnp1ge0ge0  10562  flhalf  10563  modqltm1p1mod  10639  expnbnd  10926  nn0opthlem2d  10984  ccatalpha  11191  remim  11422  remullem  11433  caucvgrelemcau  11542  caucvgre  11543  cvg1nlemcxze  11544  cvg1nlemcau  11546  cvg1nlemres  11547  recvguniqlem  11556  resqrexlem1arp  11567  resqrexlemp1rp  11568  resqrexlemf1  11570  resqrexlemfp1  11571  resqrexlemover  11572  resqrexlemdec  11573  resqrexlemlo  11575  resqrexlemcalc1  11576  resqrexlemcalc2  11577  resqrexlemnm  11580  resqrexlemcvg  11581  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemga  11585  abs00ap  11624  absext  11625  absrele  11645  abstri  11666  abs3lem  11673  amgm2  11680  qdenre  11764  maxabsle  11766  maxabslemlub  11769  maxabslemval  11770  maxcl  11772  maxltsup  11780  bdtrilem  11801  bdtri  11802  xrbdtri  11838  mulcn2  11874  fsumabs  12028  cvgratnnlembern  12086  eirraplem  12340  ltoddhalfle  12456  divalglemnqt  12483  bitscmp  12521  4sqlem12  12977  4sqlem15  12980  4sqlem16  12981  2expltfac  13014  xblss2ps  15131  cnopnap  15338  maxcncf  15342  mincncf  15343  ivthinclemlopn  15363  ivthinclemuopn  15365  hoverb  15375  ivthdichlem  15378  limcimolemlt  15391  efltlemlt  15501  cosq23lt0  15560  cosordlem  15576  lgsdirprm  15766  gausslemma2dlem1a  15790  2sqlem8  15855  qdencn  16652  trilpolemeq1  16665