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

Theorem adddi 8842
Description: Alias for ax-distr 8820, for naming consistency with adddii 8863. (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 8820 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756    x. cmul 8758
This theorem is referenced by:  adddir  8846  adddii  8863  adddid  8875  muladd11  8998  mul02lem1  9004  mul02  9006  muladd  9228  nnmulcl  9785  xadddilem  10630  expmul  11163  bernneq  11243  sqreulem  11859  isermulc2  12147  fsummulc2  12262  efexp  12397  efi4p  12433  sinadd  12460  cosadd  12461  cos2tsin  12475  cos01bnd  12482  absefib  12494  efieq1re  12495  demoivreALT  12497  odd2np1  12603  gcdmultiple  12745  opoe  12880  opeo  12882  pythagtriplem12  12895  cncrng  16411  plydivlem4  19692  sinperlem  19864  efgh  19919  cxpsqr  20066  chtub  20467  bcp1ctr  20534  gxnn0mul  20960  cnrngo  21086  cncvc  21155  hhph  21773  fsumcube  24867  distmlva  25791  stoweidlem13  27865  wallispilem4  27920
This theorem was proved from axioms:  ax-distr 8820
  Copyright terms: Public domain W3C validator