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

Theorem adddi 9582
Description: Alias for ax-distr 9560, for naming consistency with adddii 9607. (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 9560 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 973    = wceq 1379    e. wcel 1767  (class class class)co 6285   CCcc 9491    + caddc 9496    x. cmul 9498
This theorem was proved from axioms:  ax-distr 9560
This theorem is referenced by:  adddir  9588  adddii  9607  adddid  9621  muladd11  9750  mul02lem1  9756  mul02  9758  muladd  9990  nnmulcl  10560  xadddilem  11487  expmul  12180  bernneq  12261  sqreulem  13158  isermulc2  13446  fsummulc2  13565  efexp  13700  efi4p  13736  sinadd  13763  cosadd  13764  cos2tsin  13778  cos01bnd  13785  absefib  13797  efieq1re  13798  demoivreALT  13800  odd2np1  13908  gcdmultiple  14050  opoe  14197  opeo  14199  pythagtriplem12  14212  cncrng  18250  plydivlem4  22518  sinperlem  22698  cxpsqrt  22909  chtub  23312  bcp1ctr  23379  gxnn0mul  25052  cnrngo  25178  cncvc  25249  hhph  25868  fsumcube  29675
  Copyright terms: Public domain W3C validator