Theorem readdcld 8214

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

Syntax hints:   → wi 4   ∈ wcel 2201  (class class class)co 6023  ℝcr 8036   + caddc 8040

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

This theorem is referenced by:  ltadd2  8604  leadd1  8615  le2add  8629  lt2add  8630  lesub2  8642  ltsub2  8644  gt0add  8758  reapadd1  8781  apadd1  8793  mulext1  8797  recexaplem2  8837  recp1lt1  9084  cju  9146  peano5nni  9151  peano2nn  9160  div4p1lem1div2  9403  peano2z  9520  difgtsumgt  9554  eluzmn  9767  addlelt  10008  xaddf  10084  xaddval  10085  xleaddadd  10127  zltaddlt1le  10247  elincfzoext  10444  zssinfcl  10498  exbtwnzlemstep  10513  exbtwnz  10516  rebtwn2zlemstep  10518  rebtwn2z  10520  qbtwnrelemcalc  10521  flqaddz  10563  btwnzge0  10566  2tnp1ge0ge0  10567  flhalf  10568  modqltm1p1mod  10644  expnbnd  10931  nn0opthlem2d  10989  ccatalpha  11199  remim  11443  remullem  11454  caucvgrelemcau  11563  caucvgre  11564  cvg1nlemcxze  11565  cvg1nlemcau  11567  cvg1nlemres  11568  recvguniqlem  11577  resqrexlem1arp  11588  resqrexlemp1rp  11589  resqrexlemf1  11591  resqrexlemfp1  11592  resqrexlemover  11593  resqrexlemdec  11594  resqrexlemlo  11596  resqrexlemcalc1  11597  resqrexlemcalc2  11598  resqrexlemnm  11601  resqrexlemcvg  11602  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemga  11606  abs00ap  11645  absext  11646  absrele  11666  abstri  11687  abs3lem  11694  amgm2  11701  qdenre  11785  maxabsle  11787  maxabslemlub  11790  maxabslemval  11791  maxcl  11793  maxltsup  11801  bdtrilem  11822  bdtri  11823  xrbdtri  11859  mulcn2  11895  fsumabs  12049  cvgratnnlembern  12107  eirraplem  12361  ltoddhalfle  12477  divalglemnqt  12504  bitscmp  12542  4sqlem12  12998  4sqlem15  13001  4sqlem16  13002  2expltfac  13035  xblss2ps  15157  cnopnap  15364  maxcncf  15368  mincncf  15369  ivthinclemlopn  15389  ivthinclemuopn  15391  hoverb  15401  ivthdichlem  15404  limcimolemlt  15417  efltlemlt  15527  cosq23lt0  15586  cosordlem  15602  lgsdirprm  15792  gausslemma2dlem1a  15816  2sqlem8  15881  qdencn  16694  repiecelem  16696  trilpolemeq1  16711