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

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

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 7432 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1438  (class class class)co 5644  cr 7339   + caddc 7343
This theorem was proved from axioms:  ax-addrcl 7432
This theorem is referenced by:  0re  7478  readdcli  7491  readdcld  7507  axltadd  7546  peano2re  7608  cnegexlem3  7649  cnegex  7650  resubcl  7736  ltleadd  7914  ltaddsublt  8038  recexap  8112  recreclt  8351  cju  8411  nnge1  8435  addltmul  8642  avglt1  8644  avglt2  8645  avgle1  8646  avgle2  8647  nzadd  8792  irradd  9121  rpaddcl  9147  iooshf  9360  ge0addcl  9389  icoshft  9397  icoshftf1o  9398  iccshftr  9401  difelfznle  9534  elfzodifsumelfzo  9600  subfzo0  9641  serfre  9889  isermono  9894  ser3ge0  9940  bernneq  10062  faclbnd6  10140  readd  10291  imadd  10299  elicc4abs  10515  caubnd2  10538  maxabsle  10625  maxabslemval  10629  maxcl  10631  mulcn2  10688  climserle  10721  fsumrecl  10782  mertenslem2  10917  ege2le3  10948  eftlub  10967  efgt1  10974
  Copyright terms: Public domain W3C validator