Theorem readdcld 8073

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

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

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

This theorem is referenced by:  ltadd2  8463  leadd1  8474  le2add  8488  lt2add  8489  lesub2  8501  ltsub2  8503  gt0add  8617  reapadd1  8640  apadd1  8652  mulext1  8656  recexaplem2  8696  recp1lt1  8943  cju  9005  peano5nni  9010  peano2nn  9019  div4p1lem1div2  9262  peano2z  9379  difgtsumgt  9412  addlelt  9860  xaddf  9936  xaddval  9937  xleaddadd  9979  zltaddlt1le  10099  zssinfcl  10339  exbtwnzlemstep  10354  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnrelemcalc  10362  flqaddz  10404  btwnzge0  10407  2tnp1ge0ge0  10408  flhalf  10409  modqltm1p1mod  10485  expnbnd  10772  nn0opthlem2d  10830  remim  11042  remullem  11053  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemcxze  11164  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniqlem  11176  resqrexlem1arp  11187  resqrexlemp1rp  11188  resqrexlemf1  11190  resqrexlemfp1  11191  resqrexlemover  11192  resqrexlemdec  11193  resqrexlemlo  11195  resqrexlemcalc1  11196  resqrexlemcalc2  11197  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  abs00ap  11244  absext  11245  absrele  11265  abstri  11286  abs3lem  11293  amgm2  11300  qdenre  11384  maxabsle  11386  maxabslemlub  11389  maxabslemval  11390  maxcl  11392  maxltsup  11400  bdtrilem  11421  bdtri  11422  xrbdtri  11458  mulcn2  11494  fsumabs  11647  cvgratnnlembern  11705  eirraplem  11959  ltoddhalfle  12075  divalglemnqt  12102  bitscmp  12140  4sqlem12  12596  4sqlem15  12599  4sqlem16  12600  2expltfac  12633  xblss2ps  14724  cnopnap  14931  maxcncf  14935  mincncf  14936  ivthinclemlopn  14956  ivthinclemuopn  14958  hoverb  14968  ivthdichlem  14971  limcimolemlt  14984  efltlemlt  15094  cosq23lt0  15153  cosordlem  15169  lgsdirprm  15359  gausslemma2dlem1a  15383  2sqlem8  15448  qdencn  15758  trilpolemeq1  15771