Theorem mulass 10024

Description: Alias for ax-mulass 10002, for naming consistency with mulassi 10049. (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 10002	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 1037   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

This theorem was proved from axioms:  ax-mulass 10002

This theorem is referenced by:  mulid1  10037  mulassi  10049  mulassd  10063  mul12  10202  mul32  10203  mul31  10204  mul4  10205  00id  10211  divass  10703  cju  11016  div4p1lem1div2  11287  xmulasslem3  12116  mulbinom2  12984  sqoddm1div8  13028  faclbnd5  13085  bcval5  13105  remim  13857  imval2  13891  sqrlem7  13989  sqrtneglem  14007  sqreulem  14099  clim2div  14621  prodfmul  14622  prodmolem3  14663  sinhval  14884  coshval  14885  absefib  14928  efieq1re  14929  muldvds1  15006  muldvds2  15007  dvdsmulc  15009  dvdsmulcr  15011  dvdstr  15018  eulerthlem2  15487  oddprmdvds  15607  ablfacrp  18465  cncrng  19767  nmoleub2lem3  22915  cnlmod  22940  itg2mulc  23514  abssinper  24270  sinasin  24616  dchrabl  24979  bposlem6  25014  bposlem9  25017  lgsdir  25057  lgsdi  25059  2sqlem6  25148  rpvmasum2  25201  cncvcOLD  27438  ipasslem5  27690  ipasslem11  27695  dvasin  33496  pellexlem2  37394  jm2.25  37566  expgrowth  38534  2zrngmsgrp  41947  nn0sumshdiglemA  42413