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

Theorem adddi 9598
Description: Alias for ax-distr 9576, for naming consistency with adddii 9623. (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 9576 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 1395    e. wcel 1819  (class class class)co 6296   CCcc 9507    + caddc 9512    x. cmul 9514
This theorem was proved from axioms:  ax-distr 9576
This theorem is referenced by:  adddir  9604  adddii  9623  adddid  9637  muladd11  9767  mul02lem1  9773  mul02  9775  muladd  10010  nnmulcl  10579  xadddilem  11511  expmul  12213  bernneq  12294  sqreulem  13203  isermulc2  13491  fsummulc2  13610  efexp  13847  efi4p  13883  sinadd  13910  cosadd  13911  cos2tsin  13925  cos01bnd  13932  absefib  13944  efieq1re  13945  demoivreALT  13947  odd2np1  14057  gcdmultiple  14199  opoe  14346  opeo  14348  pythagtriplem12  14361  cncrng  18565  plydivlem4  22817  sinperlem  22998  cxpsqrt  23209  chtub  23612  bcp1ctr  23679  gxnn0mul  25405  cnrngo  25531  cncvc  25602  hhph  26221  fsumcube  29984  2zrngALT  32856
  Copyright terms: Public domain W3C validator