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

Theorem mulass 9476
Description: Alias for ax-mulass 9454, for naming consistency with mulassi 9501. (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 9454 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 965    = wceq 1370    e. wcel 1758  (class class class)co 6195   CCcc 9386    x. cmul 9393
This theorem was proved from axioms:  ax-mulass 9454
This theorem is referenced by:  mulid1  9489  mulassi  9501  mulassd  9515  mul12  9641  mul32  9642  mul31  9643  mul4  9644  00id  9650  divass  10118  cju  10424  xmulasslem3  11355  faclbnd5  12186  bcval5  12206  remim  12719  imval2  12753  sqrlem7  12851  sqrneglem  12869  sqreulem  12960  sinhval  13551  coshval  13552  absefib  13595  efieq1re  13596  muldvds1  13670  muldvds2  13671  dvdsmulc  13673  dvdsmulcr  13675  dvdstr  13679  eulerthlem2  13970  ablfacrp  16684  cncrng  17957  nmoleub2lem3  20797  itg2mulc  21353  abssinper  22108  sinasin  22412  dchrabl  22721  bposlem6  22756  bposlem9  22759  lgsdir  22797  lgsdi  22799  2sqlem6  22836  rpvmasum2  22889  ablomul  23989  cnrngo  24037  cncvc  24108  ipasslem5  24382  ipasslem11  24387  clim2div  27543  prodfmul  27544  prodmolem3  27585  dvasin  28623  pellexlem2  29314  jm2.25  29491  expgrowth  29752
  Copyright terms: Public domain W3C validator