Theorem readdcld 8192

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

Syntax hints:   → wi 4   ∈ wcel 2200  (class class class)co 6010  ℝcr 8014   + caddc 8018

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

This theorem is referenced by:  ltadd2  8582  leadd1  8593  le2add  8607  lt2add  8608  lesub2  8620  ltsub2  8622  gt0add  8736  reapadd1  8759  apadd1  8771  mulext1  8775  recexaplem2  8815  recp1lt1  9062  cju  9124  peano5nni  9129  peano2nn  9138  div4p1lem1div2  9381  peano2z  9498  difgtsumgt  9532  eluzmn  9745  addlelt  9981  xaddf  10057  xaddval  10058  xleaddadd  10100  zltaddlt1le  10220  elincfzoext  10416  zssinfcl  10469  exbtwnzlemstep  10484  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnrelemcalc  10492  flqaddz  10534  btwnzge0  10537  2tnp1ge0ge0  10538  flhalf  10539  modqltm1p1mod  10615  expnbnd  10902  nn0opthlem2d  10960  ccatalpha  11166  remim  11392  remullem  11403  caucvgrelemcau  11512  caucvgre  11513  cvg1nlemcxze  11514  cvg1nlemcau  11516  cvg1nlemres  11517  recvguniqlem  11526  resqrexlem1arp  11537  resqrexlemp1rp  11538  resqrexlemf1  11540  resqrexlemfp1  11541  resqrexlemover  11542  resqrexlemdec  11543  resqrexlemlo  11545  resqrexlemcalc1  11546  resqrexlemcalc2  11547  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemga  11555  abs00ap  11594  absext  11595  absrele  11615  abstri  11636  abs3lem  11643  amgm2  11650  qdenre  11734  maxabsle  11736  maxabslemlub  11739  maxabslemval  11740  maxcl  11742  maxltsup  11750  bdtrilem  11771  bdtri  11772  xrbdtri  11808  mulcn2  11844  fsumabs  11997  cvgratnnlembern  12055  eirraplem  12309  ltoddhalfle  12425  divalglemnqt  12452  bitscmp  12490  4sqlem12  12946  4sqlem15  12949  4sqlem16  12950  2expltfac  12983  xblss2ps  15099  cnopnap  15306  maxcncf  15310  mincncf  15311  ivthinclemlopn  15331  ivthinclemuopn  15333  hoverb  15343  ivthdichlem  15346  limcimolemlt  15359  efltlemlt  15469  cosq23lt0  15528  cosordlem  15544  lgsdirprm  15734  gausslemma2dlem1a  15758  2sqlem8  15823  qdencn  16509  trilpolemeq1  16522