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

Theorem mulass 8825
Description: Alias for ax-mulass 8803, for naming consistency with mulassi 8846. (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 8803 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 934    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  mulid1  8835  mulassi  8846  mulassd  8858  mul12  8978  mul32  8979  mul31  8980  mul4  8981  00id  8987  divass  9442  cju  9742  xmulasslem3  10606  faclbnd5  11311  bcval5  11330  remim  11602  imval2  11636  sqrlem7  11734  sqrneglem  11752  sqreulem  11843  sinhval  12434  coshval  12435  absefib  12478  efieq1re  12479  muldvds1  12553  muldvds2  12554  dvdsmulc  12556  dvdsmulcr  12558  dvdstr  12562  eulerthlem2  12850  ablfacrp  15301  cncrng  16395  nmoleub2lem3  18596  itg2mulc  19102  abssinper  19886  sinasin  20185  dchrabl  20493  bposlem6  20528  bposlem9  20531  lgsdir  20569  lgsdi  20571  2sqlem6  20608  rpvmasum2  20661  ablomul  21022  cnrngo  21070  cncvc  21139  ipasslem5  21413  ipasslem11  21418  pellexlem2  26915  jm2.25  27092  expgrowth  27552  fmul01lt1lem1  27714  fmul01lt1lem2  27715  stoweidlem11  27760  stoweidlem26  27775
This theorem was proved from axioms:  ax-mulass 8803
  Copyright terms: Public domain W3C validator