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

Theorem mulass 9609
Description: Alias for ax-mulass 9587, for naming consistency with mulassi 9634. (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 9587 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 974    = wceq 1405    e. wcel 1842  (class class class)co 6277   CCcc 9519    x. cmul 9526
This theorem was proved from axioms:  ax-mulass 9587
This theorem is referenced by:  mulid1  9622  mulassi  9634  mulassd  9648  mul12  9779  mul32  9780  mul31  9781  mul4  9782  00id  9788  divass  10265  cju  10571  xmulasslem3  11530  faclbnd5  12418  bcval5  12438  remim  13097  imval2  13131  sqrlem7  13229  sqrtneglem  13247  sqreulem  13339  clim2div  13848  prodfmul  13849  prodmolem3  13890  sinhval  14096  coshval  14097  absefib  14140  efieq1re  14141  muldvds1  14215  muldvds2  14216  dvdsmulc  14218  dvdsmulcr  14220  dvdstr  14225  eulerthlem2  14519  ablfacrp  17435  cncrng  18757  nmoleub2lem3  21888  itg2mulc  22444  abssinper  23201  sinasin  23543  dchrabl  23908  bposlem6  23943  bposlem9  23946  lgsdir  23984  lgsdi  23986  2sqlem6  24023  rpvmasum2  24076  ablomul  25757  cnrngo  25805  cncvc  25876  ipasslem5  26150  ipasslem11  26155  dvasin  31454  pellexlem2  35107  jm2.25  35283  expgrowth  36068  2zrngmsgrp  38245  nn0sumshdiglemA  38731
  Copyright terms: Public domain W3C validator