Theorem readdcld 8018

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

Syntax hints:   → wi 4   ∈ wcel 2160  (class class class)co 5897  ℝcr 7841   + caddc 7845

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

This theorem is referenced by:  ltadd2  8407  leadd1  8418  le2add  8432  lt2add  8433  lesub2  8445  ltsub2  8447  gt0add  8561  reapadd1  8584  apadd1  8596  mulext1  8600  recexaplem2  8640  recp1lt1  8887  cju  8949  peano5nni  8953  peano2nn  8962  div4p1lem1div2  9203  peano2z  9320  difgtsumgt  9353  addlelt  9800  xaddf  9876  xaddval  9877  xleaddadd  9919  zltaddlt1le  10039  exbtwnzlemstep  10280  exbtwnz  10283  rebtwn2zlemstep  10285  rebtwn2z  10287  qbtwnrelemcalc  10288  flqaddz  10330  btwnzge0  10333  2tnp1ge0ge0  10334  flhalf  10335  modqltm1p1mod  10409  expnbnd  10678  nn0opthlem2d  10736  remim  10904  remullem  10915  caucvgrelemcau  11024  caucvgre  11025  cvg1nlemcxze  11026  cvg1nlemcau  11028  cvg1nlemres  11029  recvguniqlem  11038  resqrexlem1arp  11049  resqrexlemp1rp  11050  resqrexlemf1  11052  resqrexlemfp1  11053  resqrexlemover  11054  resqrexlemdec  11055  resqrexlemlo  11057  resqrexlemcalc1  11058  resqrexlemcalc2  11059  resqrexlemnm  11062  resqrexlemcvg  11063  resqrexlemoverl  11065  resqrexlemglsq  11066  resqrexlemga  11067  abs00ap  11106  absext  11107  absrele  11127  abstri  11148  abs3lem  11155  amgm2  11162  qdenre  11246  maxabsle  11248  maxabslemlub  11251  maxabslemval  11252  maxcl  11254  maxltsup  11262  bdtrilem  11282  bdtri  11283  xrbdtri  11319  mulcn2  11355  fsumabs  11508  cvgratnnlembern  11566  eirraplem  11819  ltoddhalfle  11933  divalglemnqt  11960  zssinfcl  11984  4sqlem12  12437  4sqlem15  12440  4sqlem16  12441  xblss2ps  14381  cnopnap  14571  ivthinclemlopn  14591  ivthinclemuopn  14593  limcimolemlt  14610  efltlemlt  14672  cosq23lt0  14731  cosordlem  14747  lgsdirprm  14913  2sqlem8  14948  qdencn  15254  trilpolemeq1  15267