MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  readdcli Unicode version

Theorem readdcli 9630
Description: Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
Hypotheses
Ref Expression
recni.1
axri.2
Assertion
Ref Expression
readdcli

Proof of Theorem readdcli
StepHypRef Expression
1 recni.1 . 2
2 axri.2 . 2
3 readdcl 9596 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818  (class class class)co 6296   cr 9512   caddc 9516
This theorem is referenced by:  ltadd2iOLD  9737  resubcli  9904  eqneg  10289  ledivp1i  10496  ltdivp1i  10497  2re  10630  3re  10634  4re  10637  5re  10639  6re  10641  7re  10643  8re  10645  9re  10647  10re  10649  numltc  11024  nn0opthlem2  12349  hashunlei  12483  hashge2el2dif  12521  abs3lemi  13242  ef01bndlem  13919  divalglem6  14056  log2ub  23280  mumullem2  23454  bposlem8  23566  dchrvmasumlem2  23683  ex-fl  25168  norm-ii-i  26054  norm3lem  26066  nmoptrii  27013  bdophsi  27015  unierri  27023  staddi  27165  stadd3i  27167  ballotlem2  28427  itg2addnclem3  30068  fdc  30238  pellqrex  30815  stirlinglem11  31866  fouriersw  32014  zm1nn  32325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addrcl 9574
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator