Theorem readdcld 8075

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

Syntax hints:   → wi 4   ∈ wcel 2167  (class class class)co 5925  ℝcr 7897   + caddc 7901

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

This theorem is referenced by:  ltadd2  8465  leadd1  8476  le2add  8490  lt2add  8491  lesub2  8503  ltsub2  8505  gt0add  8619  reapadd1  8642  apadd1  8654  mulext1  8658  recexaplem2  8698  recp1lt1  8945  cju  9007  peano5nni  9012  peano2nn  9021  div4p1lem1div2  9264  peano2z  9381  difgtsumgt  9414  addlelt  9862  xaddf  9938  xaddval  9939  xleaddadd  9981  zltaddlt1le  10101  zssinfcl  10341  exbtwnzlemstep  10356  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnrelemcalc  10364  flqaddz  10406  btwnzge0  10409  2tnp1ge0ge0  10410  flhalf  10411  modqltm1p1mod  10487  expnbnd  10774  nn0opthlem2d  10832  remim  11044  remullem  11055  caucvgrelemcau  11164  caucvgre  11165  cvg1nlemcxze  11166  cvg1nlemcau  11168  cvg1nlemres  11169  recvguniqlem  11178  resqrexlem1arp  11189  resqrexlemp1rp  11190  resqrexlemf1  11192  resqrexlemfp1  11193  resqrexlemover  11194  resqrexlemdec  11195  resqrexlemlo  11197  resqrexlemcalc1  11198  resqrexlemcalc2  11199  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  abs00ap  11246  absext  11247  absrele  11267  abstri  11288  abs3lem  11295  amgm2  11302  qdenre  11386  maxabsle  11388  maxabslemlub  11391  maxabslemval  11392  maxcl  11394  maxltsup  11402  bdtrilem  11423  bdtri  11424  xrbdtri  11460  mulcn2  11496  fsumabs  11649  cvgratnnlembern  11707  eirraplem  11961  ltoddhalfle  12077  divalglemnqt  12104  bitscmp  12142  4sqlem12  12598  4sqlem15  12601  4sqlem16  12602  2expltfac  12635  xblss2ps  14748  cnopnap  14955  maxcncf  14959  mincncf  14960  ivthinclemlopn  14980  ivthinclemuopn  14982  hoverb  14992  ivthdichlem  14995  limcimolemlt  15008  efltlemlt  15118  cosq23lt0  15177  cosordlem  15193  lgsdirprm  15383  gausslemma2dlem1a  15407  2sqlem8  15472  qdencn  15784  trilpolemeq1  15797