Theorem mulass 10960

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1542   ∈ wcel 2110  (class class class)co 7271  ℂcc 10870   · cmul 10877

This theorem was proved from axioms:  ax-mulass 10938

This theorem is referenced by:  mulid1  10974  mulassi  10987  mulassd  10999  mul12  11140  mul32  11141  mul31  11142  mul4  11143  00id  11150  divass  11651  cju  11969  div4p1lem1div2  12228  xmulasslem3  13019  mulbinom2  13936  sqoddm1div8  13956  faclbnd5  14010  bcval5  14030  remim  14826  imval2  14860  sqrlem7  14958  sqrtneglem  14976  sqreulem  15069  clim2div  15599  prodfmul  15600  prodmolem3  15641  sinhval  15861  coshval  15862  absefib  15905  efieq1re  15906  muldvds1  15988  muldvds2  15989  dvdsmulc  15991  dvdsmulcr  15993  dvdstr  16001  eulerthlem2  16481  oddprmdvds  16602  ablfacrp  19667  cncrng  20617  nmoleub2lem3  24276  cnlmod  24301  itg2mulc  24910  abssinper  25675  sinasin  26037  dchrabl  26400  bposlem6  26435  bposlem9  26438  2sqlem6  26569  rpvmasum2  26658  cncvcOLD  28941  ipasslem5  29193  ipasslem11  29198  dvasin  35857  facp2  40096  fac2xp3  40157  pellexlem2  40649  jm2.25  40818  expgrowth  41923  2zrngmsgrp  45474  nn0sumshdiglemA  45934