Theorem readdcl 7099

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

Assertion

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

Proof of Theorem readdcl

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

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

This theorem was proved from axioms:  ax-addrcl 7073

This theorem is referenced by:  0re  7119  readdcli  7132  readdcld  7148  axltadd  7182  peano2re  7244  cnegexlem3  7285  cnegex  7286  resubcl  7372  ltleadd  7550  ltaddsublt  7671  recexap  7743  recreclt  7978  cju  8038  nnge1  8062  addltmul  8267  avglt1  8269  avglt2  8270  avgle1  8271  avgle2  8272  nzadd  8403  irradd  8731  rpaddcl  8757  iooshf  8975  ge0addcl  9004  icoshft  9012  icoshftf1o  9013  iccshftr  9016  difelfznle  9146  elfzodifsumelfzo  9210  subfzo0  9251  iserfre  9454  isermono  9457  serige0  9473  serile  9474  bernneq  9593  faclbnd6  9671  readd  9756  imadd  9764  elicc4abs  9980  caubnd2  10003  maxabsle  10090  maxabslemval  10094  maxcl  10096  mulcn2  10151  iserile  10180  climserile  10183