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

Theorem adddi 8826
Description: Alias for ax-distr 8804, for naming consistency with adddii 8847. (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 8804 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 934    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742
This theorem is referenced by:  adddir  8830  adddii  8847  adddid  8859  muladd11  8982  mul02lem1  8988  mul02  8990  muladd  9212  nnmulcl  9769  xadddilem  10614  expmul  11147  bernneq  11227  sqreulem  11843  isermulc2  12131  fsummulc2  12246  efexp  12381  efi4p  12417  sinadd  12444  cosadd  12445  cos2tsin  12459  cos01bnd  12466  absefib  12478  efieq1re  12479  demoivreALT  12481  odd2np1  12587  gcdmultiple  12729  opoe  12864  opeo  12866  pythagtriplem12  12879  cncrng  16395  plydivlem4  19676  sinperlem  19848  efgh  19903  cxpsqr  20050  chtub  20451  bcp1ctr  20518  gxnn0mul  20944  cnrngo  21070  cncvc  21139  hhph  21757  fsumcube  24795  distmlva  25688  stoweidlem13  27762  wallispilem4  27817
This theorem was proved from axioms:  ax-distr 8804
  Copyright terms: Public domain W3C validator