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

Theorem mulass 8841
Description: Alias for ax-mulass 8819, for naming consistency with mulassi 8862. (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 8819 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  mulid1  8851  mulassi  8862  mulassd  8874  mul12  8994  mul32  8995  mul31  8996  mul4  8997  00id  9003  divass  9458  cju  9758  xmulasslem3  10622  faclbnd5  11327  bcval5  11346  remim  11618  imval2  11652  sqrlem7  11750  sqrneglem  11768  sqreulem  11859  sinhval  12450  coshval  12451  absefib  12494  efieq1re  12495  muldvds1  12569  muldvds2  12570  dvdsmulc  12572  dvdsmulcr  12574  dvdstr  12578  eulerthlem2  12866  ablfacrp  15317  cncrng  16411  nmoleub2lem3  18612  itg2mulc  19118  abssinper  19902  sinasin  20201  dchrabl  20509  bposlem6  20544  bposlem9  20547  lgsdir  20585  lgsdi  20587  2sqlem6  20624  rpvmasum2  20677  ablomul  21038  cnrngo  21086  cncvc  21155  ipasslem5  21429  ipasslem11  21434  prodmolem3  24156  pellexlem2  27017  jm2.25  27194  expgrowth  27654  fmul01lt1lem1  27816  fmul01lt1lem2  27817  stoweidlem11  27862  stoweidlem26  27877
This theorem was proved from axioms:  ax-mulass 8819
  Copyright terms: Public domain W3C validator