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

Theorem mulass 9366
Description: Alias for ax-mulass 9344, for naming consistency with mulassi 9391. (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 9344 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 960    = wceq 1364    e. wcel 1761  (class class class)co 6090   CCcc 9276    x. cmul 9283
This theorem was proved from axioms:  ax-mulass 9344
This theorem is referenced by:  mulid1  9379  mulassi  9391  mulassd  9405  mul12  9531  mul32  9532  mul31  9533  mul4  9534  00id  9540  divass  10008  cju  10314  xmulasslem3  11245  faclbnd5  12070  bcval5  12090  remim  12602  imval2  12636  sqrlem7  12734  sqrneglem  12752  sqreulem  12843  sinhval  13434  coshval  13435  absefib  13478  efieq1re  13479  muldvds1  13553  muldvds2  13554  dvdsmulc  13556  dvdsmulcr  13558  dvdstr  13562  eulerthlem2  13853  ablfacrp  16557  cncrng  17796  nmoleub2lem3  20629  itg2mulc  21184  abssinper  21939  sinasin  22243  dchrabl  22552  bposlem6  22587  bposlem9  22590  lgsdir  22628  lgsdi  22630  2sqlem6  22667  rpvmasum2  22720  ablomul  23777  cnrngo  23825  cncvc  23896  ipasslem5  24170  ipasslem11  24175  clim2div  27333  prodfmul  27334  prodmolem3  27375  dvasin  28405  pellexlem2  29096  jm2.25  29273  expgrowth  29534
  Copyright terms: Public domain W3C validator