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

Theorem mulass 9070
Description: Alias for ax-mulass 9048, for naming consistency with mulassi 9091. (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 9048 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 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980    x. cmul 8987
This theorem is referenced by:  mulid1  9080  mulassi  9091  mulassd  9103  mul12  9224  mul32  9225  mul31  9226  mul4  9227  00id  9233  divass  9688  cju  9988  xmulasslem3  10857  faclbnd5  11581  bcval5  11601  remim  11914  imval2  11948  sqrlem7  12046  sqrneglem  12064  sqreulem  12155  sinhval  12747  coshval  12748  absefib  12791  efieq1re  12792  muldvds1  12866  muldvds2  12867  dvdsmulc  12869  dvdsmulcr  12871  dvdstr  12875  eulerthlem2  13163  ablfacrp  15616  cncrng  16714  nmoleub2lem3  19115  itg2mulc  19631  abssinper  20418  sinasin  20721  dchrabl  21030  bposlem6  21065  bposlem9  21068  lgsdir  21106  lgsdi  21108  2sqlem6  21145  rpvmasum2  21198  ablomul  21935  cnrngo  21983  cncvc  22054  ipasslem5  22328  ipasslem11  22333  clim2div  25209  prodfmul  25210  prodmolem3  25251  pellexlem2  26884  jm2.25  27061  expgrowth  27520
This theorem was proved from axioms:  ax-mulass 9048
  Copyright terms: Public domain W3C validator