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

Theorem mulass 9034
Description: Alias for ax-mulass 9012, for naming consistency with mulassi 9055. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )

Proof of Theorem mulass
StepHypRef Expression
1 ax-mulass 9012 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  mulid1  9044  mulassi  9055  mulassd  9067  mul12  9188  mul32  9189  mul31  9190  mul4  9191  00id  9197  divass  9652  cju  9952  xmulasslem3  10821  faclbnd5  11544  bcval5  11564  remim  11877  imval2  11911  sqrlem7  12009  sqrneglem  12027  sqreulem  12118  sinhval  12710  coshval  12711  absefib  12754  efieq1re  12755  muldvds1  12829  muldvds2  12830  dvdsmulc  12832  dvdsmulcr  12834  dvdstr  12838  eulerthlem2  13126  ablfacrp  15579  cncrng  16677  nmoleub2lem3  19076  itg2mulc  19592  abssinper  20379  sinasin  20682  dchrabl  20991  bposlem6  21026  bposlem9  21029  lgsdir  21067  lgsdi  21069  2sqlem6  21106  rpvmasum2  21159  ablomul  21896  cnrngo  21944  cncvc  22015  ipasslem5  22289  ipasslem11  22294  clim2div  25170  prodfmul  25171  prodmolem3  25212  pellexlem2  26783  jm2.25  26960  expgrowth  27420
This theorem was proved from axioms:  ax-mulass 9012
  Copyright terms: Public domain W3C validator