Theorem readdcl 7998

Description: Alias for ax-addrcl 7969, for naming consistency with readdcli 8032. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
readdcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl

Step	Hyp	Ref	Expression
1		ax-addrcl 7969	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164  (class class class)co 5918  ℝcr 7871   + caddc 7875

This theorem was proved from axioms:  ax-addrcl 7969

This theorem is referenced by:  0re  8019  readdcli  8032  readdcld  8049  axltadd  8089  peano2re  8155  cnegexlem3  8196  cnegex  8197  resubcl  8283  ltleadd  8465  ltaddsublt  8590  recexap  8672  recreclt  8919  cju  8980  nnge1  9005  addltmul  9219  avglt1  9221  avglt2  9222  avgle1  9223  avgle2  9224  nzadd  9369  irradd  9711  rpaddcl  9743  xaddnemnf  9923  xaddnepnf  9924  xnegdi  9934  xaddass  9935  xltadd1  9942  iooshf  10018  ge0addcl  10047  icoshft  10056  icoshftf1o  10057  iccshftr  10060  difelfznle  10201  elfzodifsumelfzo  10268  subfzo0  10309  serfre  10555  ser3mono  10558  ser3ge0  10607  bernneq  10731  faclbnd6  10815  readd  11013  imadd  11021  elicc4abs  11238  caubnd2  11261  maxabsle  11348  maxabslemval  11352  maxcl  11354  mulcn2  11455  climserle  11488  fsumrecl  11544  mertenslem2  11679  ege2le3  11814  eftlub  11833  efgt1  11840  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  xmeter  14604  bl2ioo  14710  ioo2bl  14711  ioo2blex  14712  blssioo  14713  tangtx  14973  relogmul  15004