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

Theorem mulass 9013
Description: Alias for ax-mulass 8991, for naming consistency with mulassi 9034. (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 8991 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 1717  (class class class)co 6022   CCcc 8923    x. cmul 8930
This theorem is referenced by:  mulid1  9023  mulassi  9034  mulassd  9046  mul12  9166  mul32  9167  mul31  9168  mul4  9169  00id  9175  divass  9630  cju  9930  xmulasslem3  10799  faclbnd5  11518  bcval5  11538  remim  11851  imval2  11885  sqrlem7  11983  sqrneglem  12001  sqreulem  12092  sinhval  12684  coshval  12685  absefib  12728  efieq1re  12729  muldvds1  12803  muldvds2  12804  dvdsmulc  12806  dvdsmulcr  12808  dvdstr  12812  eulerthlem2  13100  ablfacrp  15553  cncrng  16647  nmoleub2lem3  18996  itg2mulc  19508  abssinper  20295  sinasin  20598  dchrabl  20907  bposlem6  20942  bposlem9  20945  lgsdir  20983  lgsdi  20985  2sqlem6  21022  rpvmasum2  21075  ablomul  21793  cnrngo  21841  cncvc  21912  ipasslem5  22186  ipasslem11  22191  clim2div  24998  prodfmul  24999  prodmolem3  25040  pellexlem2  26586  jm2.25  26763  expgrowth  27223
This theorem was proved from axioms:  ax-mulass 8991
  Copyright terms: Public domain W3C validator