Theorem mulass 11089

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   · cmul 11006

This theorem was proved from axioms:  ax-mulass 11067

This theorem is referenced by:  mulrid  11105  mulassi  11118  mulassd  11130  mul12  11273  mul32  11274  mul31  11275  mul4  11276  00id  11283  divass  11789  cju  12116  div4p1lem1div2  12371  xmulasslem3  13180  mulbinom2  14125  sqoddm1div8  14145  faclbnd5  14200  bcval5  14220  remim  15019  imval2  15053  01sqrexlem7  15150  sqrtneglem  15168  sqreulem  15262  clim2div  15791  prodfmul  15792  prodmolem3  15835  sinhval  16058  coshval  16059  absefib  16102  efieq1re  16103  muldvds1  16186  muldvds2  16187  dvdsmulc  16189  dvdsmulcr  16191  dvdstr  16200  eulerthlem2  16688  oddprmdvds  16810  ablfacrp  19975  cncrng  21320  cncrngOLD  21321  nmoleub2lem3  25037  cnlmod  25062  itg2mulc  25670  abssinper  26452  sinasin  26821  dchrabl  27187  bposlem6  27222  bposlem9  27225  2sqlem6  27356  rpvmasum2  27445  cncvcOLD  30555  ipasslem5  30807  ipasslem11  30812  dvasin  37744  facp2  42176  pellexlem2  42863  jm2.25  43032  expgrowth  44368  2zrngmsgrp  48284  nn0sumshdiglemA  48651