Theorem readdcld 7148

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

Syntax hints:   → wi 4   ∈ wcel 1433  (class class class)co 5532  ℝcr 6980   + caddc 6984

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

This theorem is referenced by:  ltadd2  7523  leadd1  7534  le2add  7548  lt2add  7549  lesub2  7561  ltsub2  7563  gt0add  7673  reapadd1  7696  apadd1  7708  mulext1  7712  recexaplem2  7742  recp1lt1  7977  cju  8038  peano5nni  8042  peano2nn  8051  div4p1lem1div2  8284  peano2z  8387  addlelt  8839  zltaddlt1le  9028  qbtwnzlemstep  9257  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnrelemcalc  9264  flqaddz  9299  btwnzge0  9302  2tnp1ge0ge0  9303  flhalf  9304  modqltm1p1mod  9378  expnbnd  9596  nn0opthlem2d  9648  remim  9747  remullem  9758  caucvgrelemcau  9866  caucvgre  9867  cvg1nlemcxze  9868  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniqlem  9880  resqrexlem1arp  9891  resqrexlemp1rp  9892  resqrexlemf1  9894  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  abs00ap  9948  absext  9949  absrele  9969  abstri  9990  abs3lem  9997  amgm2  10004  qdenre  10088  maxabsle  10090  maxabslemlub  10093  maxabslemval  10094  maxcl  10096  maxltsup  10104  mulcn2  10151  ltoddhalfle  10293  divalglemnqt  10320  zssinfcl  10344  qdencn  10785