Theorem readdcld 8202

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6013  ℝcr 8024   + caddc 8028

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

This theorem is referenced by:  ltadd2  8592  leadd1  8603  le2add  8617  lt2add  8618  lesub2  8630  ltsub2  8632  gt0add  8746  reapadd1  8769  apadd1  8781  mulext1  8785  recexaplem2  8825  recp1lt1  9072  cju  9134  peano5nni  9139  peano2nn  9148  div4p1lem1div2  9391  peano2z  9508  difgtsumgt  9542  eluzmn  9755  addlelt  9996  xaddf  10072  xaddval  10073  xleaddadd  10115  zltaddlt1le  10235  elincfzoext  10431  zssinfcl  10485  exbtwnzlemstep  10500  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnrelemcalc  10508  flqaddz  10550  btwnzge0  10553  2tnp1ge0ge0  10554  flhalf  10555  modqltm1p1mod  10631  expnbnd  10918  nn0opthlem2d  10976  ccatalpha  11183  remim  11414  remullem  11425  caucvgrelemcau  11534  caucvgre  11535  cvg1nlemcxze  11536  cvg1nlemcau  11538  cvg1nlemres  11539  recvguniqlem  11548  resqrexlem1arp  11559  resqrexlemp1rp  11560  resqrexlemf1  11562  resqrexlemfp1  11563  resqrexlemover  11564  resqrexlemdec  11565  resqrexlemlo  11567  resqrexlemcalc1  11568  resqrexlemcalc2  11569  resqrexlemnm  11572  resqrexlemcvg  11573  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemga  11577  abs00ap  11616  absext  11617  absrele  11637  abstri  11658  abs3lem  11665  amgm2  11672  qdenre  11756  maxabsle  11758  maxabslemlub  11761  maxabslemval  11762  maxcl  11764  maxltsup  11772  bdtrilem  11793  bdtri  11794  xrbdtri  11830  mulcn2  11866  fsumabs  12019  cvgratnnlembern  12077  eirraplem  12331  ltoddhalfle  12447  divalglemnqt  12474  bitscmp  12512  4sqlem12  12968  4sqlem15  12971  4sqlem16  12972  2expltfac  13005  xblss2ps  15121  cnopnap  15328  maxcncf  15332  mincncf  15333  ivthinclemlopn  15353  ivthinclemuopn  15355  hoverb  15365  ivthdichlem  15368  limcimolemlt  15381  efltlemlt  15491  cosq23lt0  15550  cosordlem  15566  lgsdirprm  15756  gausslemma2dlem1a  15780  2sqlem8  15845  qdencn  16581  trilpolemeq1  16594