Theorem mulass 7972

Description: Alias for ax-mulass 7944, for naming consistency with mulassi 7996. (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

Step	Hyp	Ref	Expression
1		ax-mulass 7944	1 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Syntax hints:   -> wi 4   /\ w3a 980   = wceq 1364   e. wcel 2160  (class class class)co 5896   CCcc 7839   x. cmul 7846

This theorem was proved from axioms:  ax-mulass 7944

This theorem is referenced by:  mulrid  7984  mulassi  7996  mulassd  8011  mul12  8116  mul32  8117  mul31  8118  mul4  8119  rimul  8572  divassap  8677  cju  8948  div4p1lem1div2  9202  mulbinom2  10668  sqoddm1div8  10705  remim  10901  imval2  10935  clim2divap  11580  prod3fmul  11581  prodmodclem3  11615  absefib  11810  efieq1re  11811  muldvds1  11855  muldvds2  11856  dvdsmulc  11858  dvdstr  11867  oddprmdvds  12386  cncrng  13872  abssinper  14724  2sqlem6  14925