Theorem mulass 10062

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  (class class class)co 6690  ℂcc 9972   · cmul 9979

This theorem was proved from axioms:  ax-mulass 10040

This theorem is referenced by:  mulid1  10075  mulassi  10087  mulassd  10101  mul12  10240  mul32  10241  mul31  10242  mul4  10243  00id  10249  divass  10741  cju  11054  div4p1lem1div2  11325  xmulasslem3  12154  mulbinom2  13024  sqoddm1div8  13068  faclbnd5  13125  bcval5  13145  remim  13901  imval2  13935  sqrlem7  14033  sqrtneglem  14051  sqreulem  14143  clim2div  14665  prodfmul  14666  prodmolem3  14707  sinhval  14928  coshval  14929  absefib  14972  efieq1re  14973  muldvds1  15053  muldvds2  15054  dvdsmulc  15056  dvdsmulcr  15058  dvdstr  15065  eulerthlem2  15534  oddprmdvds  15654  ablfacrp  18511  cncrng  19815  nmoleub2lem3  22961  cnlmod  22986  itg2mulc  23559  abssinper  24315  sinasin  24661  dchrabl  25024  bposlem6  25059  bposlem9  25062  lgsdir  25102  lgsdi  25104  2sqlem6  25193  rpvmasum2  25246  cncvcOLD  27566  ipasslem5  27818  ipasslem11  27823  dvasin  33626  pellexlem2  37711  jm2.25  37883  expgrowth  38851  2zrngmsgrp  42272  nn0sumshdiglemA  42738