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

Theorem adddi 9043
Description: Alias for ax-distr 9021, for naming consistency with adddii 9064. (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 9021 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 936    = wceq 1649    e. wcel 1721  (class class class)co 6048   CCcc 8952    + caddc 8957    x. cmul 8959
This theorem is referenced by:  adddir  9047  adddii  9064  adddid  9076  muladd11  9200  mul02lem1  9206  mul02  9208  muladd  9430  nnmulcl  9987  xadddilem  10837  expmul  11388  bernneq  11468  sqreulem  12126  isermulc2  12414  fsummulc2  12530  efexp  12665  efi4p  12701  sinadd  12728  cosadd  12729  cos2tsin  12743  cos01bnd  12750  absefib  12762  efieq1re  12763  demoivreALT  12765  odd2np1  12871  gcdmultiple  13013  opoe  13148  opeo  13150  pythagtriplem12  13163  cncrng  16685  plydivlem4  20174  sinperlem  20349  efgh  20404  cxpsqr  20555  chtub  20957  bcp1ctr  21024  gxnn0mul  21826  cnrngo  21952  cncvc  22023  hhph  22641  fsumcube  26018
This theorem was proved from axioms:  ax-distr 9021
  Copyright terms: Public domain W3C validator