Theorem mulass 10627

Description: Alias for ax-mulass 10605, for naming consistency with mulassi 10654. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulass

Step	Hyp	Ref	Expression
1		ax-mulass 10605	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

This theorem was proved from axioms:  ax-mulass 10605

This theorem is referenced by:  mulid1  10641  mulassi  10654  mulassd  10666  mul12  10807  mul32  10808  mul31  10809  mul4  10810  00id  10817  divass  11318  cju  11636  div4p1lem1div2  11895  xmulasslem3  12682  mulbinom2  13587  sqoddm1div8  13607  faclbnd5  13661  bcval5  13681  remim  14478  imval2  14512  sqrlem7  14610  sqrtneglem  14628  sqreulem  14721  clim2div  15247  prodfmul  15248  prodmolem3  15289  sinhval  15509  coshval  15510  absefib  15553  efieq1re  15554  muldvds1  15636  muldvds2  15637  dvdsmulc  15639  dvdsmulcr  15641  dvdstr  15648  eulerthlem2  16121  oddprmdvds  16241  ablfacrp  19190  cncrng  20568  nmoleub2lem3  23721  cnlmod  23746  itg2mulc  24350  abssinper  25108  sinasin  25469  dchrabl  25832  bposlem6  25867  bposlem9  25870  2sqlem6  26001  rpvmasum2  26090  cncvcOLD  28362  ipasslem5  28614  ipasslem11  28619  dvasin  34980  fac2xp3  39101  facp2  39102  pellexlem2  39434  jm2.25  39603  expgrowth  40674  2zrngmsgrp  44225  nn0sumshdiglemA  44686