ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  readdcl GIF version

Theorem readdcl 7007
Description: Alias for ax-addrcl 6981, for naming consistency with readdcli 7040. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 6981 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  (class class class)co 5512  cr 6888   + caddc 6892
This theorem was proved from axioms:  ax-addrcl 6981
This theorem is referenced by:  0re  7027  readdcli  7040  readdcld  7055  axltadd  7089  peano2re  7149  cnegexlem3  7188  cnegex  7189  resubcl  7275  ltleadd  7441  ltaddsublt  7562  recexap  7634  recreclt  7866  cju  7913  nnge1  7937  addltmul  8161  avglt1  8163  avglt2  8164  avgle1  8165  avgle2  8166  irradd  8580  rpaddcl  8606  iooshf  8821  ge0addcl  8850  icoshft  8858  icoshftf1o  8859  iccshftr  8862  difelfznle  8993  elfzodifsumelfzo  9057  subfzo0  9097  iserfre  9234  isermono  9237  serige0  9252  serile  9253  bernneq  9369  readd  9469  imadd  9477  elicc4abs  9690  caubnd2  9713  mulcn2  9833  iserile  9862  climserile  9865
  Copyright terms: Public domain W3C validator