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

Theorem mulass 9576
Description: Alias for ax-mulass 9554, for naming consistency with mulassi 9601. (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 9554 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 973    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    x. cmul 9493
This theorem was proved from axioms:  ax-mulass 9554
This theorem is referenced by:  mulid1  9589  mulassi  9601  mulassd  9615  mul12  9741  mul32  9742  mul31  9743  mul4  9744  00id  9750  divass  10221  cju  10528  xmulasslem3  11474  faclbnd5  12340  bcval5  12360  remim  12909  imval2  12943  sqrlem7  13041  sqrtneglem  13059  sqreulem  13151  sinhval  13746  coshval  13747  absefib  13790  efieq1re  13791  muldvds1  13865  muldvds2  13866  dvdsmulc  13868  dvdsmulcr  13870  dvdstr  13874  eulerthlem2  14167  ablfacrp  16907  cncrng  18210  nmoleub2lem3  21333  itg2mulc  21889  abssinper  22644  sinasin  22948  dchrabl  23257  bposlem6  23292  bposlem9  23295  lgsdir  23333  lgsdi  23335  2sqlem6  23372  rpvmasum2  23425  ablomul  25033  cnrngo  25081  cncvc  25152  ipasslem5  25426  ipasslem11  25431  clim2div  28600  prodfmul  28601  prodmolem3  28642  dvasin  29680  pellexlem2  30370  jm2.25  30545  expgrowth  30840
  Copyright terms: Public domain W3C validator