Theorem readdcld 7055

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

Syntax hints:   → wi 4   ∈ wcel 1393  (class class class)co 5512  ℝcr 6888   + caddc 6892

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

This theorem is referenced by:  ltadd2  7416  leadd1  7425  le2add  7439  lt2add  7440  lesub2  7452  ltsub2  7454  gt0add  7564  reapadd1  7587  apadd1  7599  mulext1  7603  recexaplem2  7633  recp1lt1  7865  cju  7913  peano5nni  7917  peano2nn  7926  div4p1lem1div2  8177  peano2z  8281  qbtwnzlemstep  9103  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  qbtwnrelemcalc  9110  flqaddz  9139  btwnzge0  9142  2tnp1ge0ge0  9143  flhalf  9144  expnbnd  9372  remim  9460  remullem  9471  caucvgrelemcau  9579  caucvgre  9580  cvg1nlemcxze  9581  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniqlem  9592  resqrexlem1arp  9603  resqrexlemp1rp  9604  resqrexlemf1  9606  resqrexlemfp1  9607  resqrexlemover  9608  resqrexlemdec  9609  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  abs00ap  9660  absext  9661  absrele  9679  abstri  9700  abs3lem  9707  amgm2  9714  qdenre  9798  mulcn2  9833  qdencn  10124