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

Theorem adddi 9110
Description: Alias for ax-distr 9088, for naming consistency with adddii 9131. (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 9088 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937    = wceq 1653    e. wcel 1727  (class class class)co 6110   CCcc 9019    + caddc 9024    x. cmul 9026
This theorem is referenced by:  adddir  9114  adddii  9131  adddid  9143  muladd11  9267  mul02lem1  9273  mul02  9275  muladd  9497  nnmulcl  10054  xadddilem  10904  expmul  11456  bernneq  11536  sqreulem  12194  isermulc2  12482  fsummulc2  12598  efexp  12733  efi4p  12769  sinadd  12796  cosadd  12797  cos2tsin  12811  cos01bnd  12818  absefib  12830  efieq1re  12831  demoivreALT  12833  odd2np1  12939  gcdmultiple  13081  opoe  13216  opeo  13218  pythagtriplem12  13231  cncrng  16753  plydivlem4  20244  sinperlem  20419  efgh  20474  cxpsqr  20625  chtub  21027  bcp1ctr  21094  gxnn0mul  21896  cnrngo  22022  cncvc  22093  hhph  22711  fsumcube  26137
This theorem was proved from axioms:  ax-distr 9088
  Copyright terms: Public domain W3C validator