Theorem mulass 10614

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

This theorem was proved from axioms:  ax-mulass 10592

This theorem is referenced by:  mulid1  10628  mulassi  10641  mulassd  10653  mul12  10794  mul32  10795  mul31  10796  mul4  10797  00id  10804  divass  11305  cju  11621  div4p1lem1div2  11880  xmulasslem3  12667  mulbinom2  13580  sqoddm1div8  13600  faclbnd5  13654  bcval5  13674  remim  14468  imval2  14502  sqrlem7  14600  sqrtneglem  14618  sqreulem  14711  clim2div  15237  prodfmul  15238  prodmolem3  15279  sinhval  15499  coshval  15500  absefib  15543  efieq1re  15544  muldvds1  15626  muldvds2  15627  dvdsmulc  15629  dvdsmulcr  15631  dvdstr  15638  eulerthlem2  16109  oddprmdvds  16229  ablfacrp  19181  cncrng  20112  nmoleub2lem3  23720  cnlmod  23745  itg2mulc  24351  abssinper  25113  sinasin  25475  dchrabl  25838  bposlem6  25873  bposlem9  25876  2sqlem6  26007  rpvmasum2  26096  cncvcOLD  28366  ipasslem5  28618  ipasslem11  28623  dvasin  35141  facp2  39347  fac2xp3  39385  pellexlem2  39771  jm2.25  39940  expgrowth  41039  2zrngmsgrp  44571  nn0sumshdiglemA  45033