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

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

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 7135 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  (class class class)co 5543  cr 7042   + caddc 7046
This theorem was proved from axioms:  ax-addrcl 7135
This theorem is referenced by:  0re  7181  readdcli  7194  readdcld  7210  axltadd  7249  peano2re  7311  cnegexlem3  7352  cnegex  7353  resubcl  7439  ltleadd  7617  ltaddsublt  7738  recexap  7810  recreclt  8045  cju  8105  nnge1  8129  addltmul  8334  avglt1  8336  avglt2  8337  avgle1  8338  avgle2  8339  nzadd  8484  irradd  8812  rpaddcl  8838  iooshf  9051  ge0addcl  9080  icoshft  9088  icoshftf1o  9089  iccshftr  9092  difelfznle  9223  elfzodifsumelfzo  9287  subfzo0  9328  iserfre  9550  isermono  9553  serige0  9570  serile  9571  bernneq  9690  faclbnd6  9768  readd  9894  imadd  9902  elicc4abs  10118  caubnd2  10141  maxabsle  10228  maxabslemval  10232  maxcl  10234  mulcn2  10289  iserile  10318  climserile  10321
  Copyright terms: Public domain W3C validator