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

Theorem readdcl 7065
Description: Alias for ax-addrcl 7039, for naming consistency with readdcli 7098. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
readdcl  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )

Proof of Theorem readdcl
StepHypRef Expression
1 ax-addrcl 7039 1  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    e. wcel 1409  (class class class)co 5540   RRcr 6946    + caddc 6950
This theorem was proved from axioms:  ax-addrcl 7039
This theorem is referenced by:  0re  7085  readdcli  7098  readdcld  7114  axltadd  7148  peano2re  7210  cnegexlem3  7251  cnegex  7252  resubcl  7338  ltleadd  7515  ltaddsublt  7636  recexap  7708  recreclt  7941  cju  7989  nnge1  8013  addltmul  8218  avglt1  8220  avglt2  8221  avgle1  8222  avgle2  8223  nzadd  8354  irradd  8678  rpaddcl  8704  iooshf  8922  ge0addcl  8951  icoshft  8959  icoshftf1o  8960  iccshftr  8963  difelfznle  9095  elfzodifsumelfzo  9159  subfzo0  9199  iserfre  9398  isermono  9401  serige0  9417  serile  9418  bernneq  9537  faclbnd6  9612  readd  9697  imadd  9705  elicc4abs  9921  caubnd2  9944  mulcn2  10064  iserile  10093  climserile  10096
  Copyright terms: Public domain W3C validator