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

Theorem adddi 9602
Description: Alias for ax-distr 9580, for naming consistency with adddii 9627. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 9580 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516   cmul 9518
This theorem is referenced by:  adddir  9608  adddii  9627  adddid  9641  muladd11  9771  mul02lem1  9777  mul02  9779  muladd  10014  nnmulcl  10584  xadddilem  11515  expmul  12211  bernneq  12292  sqreulem  13192  isermulc2  13480  fsummulc2  13599  efexp  13836  efi4p  13872  sinadd  13899  cosadd  13900  cos2tsin  13914  cos01bnd  13921  absefib  13933  efieq1re  13934  demoivreALT  13936  odd2np1  14046  gcdmultiple  14188  opoe  14335  opeo  14337  pythagtriplem12  14350  cncrng  18439  plydivlem4  22692  sinperlem  22873  cxpsqrt  23084  chtub  23487  bcp1ctr  23554  gxnn0mul  25279  cnrngo  25405  cncvc  25476  hhph  26095  fsumcube  29822  2zrngALT  32754
This theorem was proved from axioms:  ax-distr 9580
  Copyright terms: Public domain W3C validator