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

Theorem adddi 9392
Description: Alias for ax-distr 9370, for naming consistency with adddii 9417. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 9370 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965    = wceq 1369    e. wcel 1756  (class class class)co 6112   CCcc 9301    + caddc 9306    x. cmul 9308
This theorem was proved from axioms:  ax-distr 9370
This theorem is referenced by:  adddir  9398  adddii  9417  adddid  9431  muladd11  9560  mul02lem1  9566  mul02  9568  muladd  9798  nnmulcl  10366  xadddilem  11278  expmul  11930  bernneq  12011  sqreulem  12868  isermulc2  13156  fsummulc2  13272  efexp  13406  efi4p  13442  sinadd  13469  cosadd  13470  cos2tsin  13484  cos01bnd  13491  absefib  13503  efieq1re  13504  demoivreALT  13506  odd2np1  13613  gcdmultiple  13755  opoe  13899  opeo  13901  pythagtriplem12  13914  cncrng  17859  plydivlem4  21784  sinperlem  21964  efgh  22019  cxpsqr  22170  chtub  22573  bcp1ctr  22640  gxnn0mul  23786  cnrngo  23912  cncvc  23983  hhph  24602  fsumcube  28225
  Copyright terms: Public domain W3C validator