Theorem mulass 10890

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

This theorem was proved from axioms:  ax-mulass 10868

This theorem is referenced by:  mulid1  10904  mulassi  10917  mulassd  10929  mul12  11070  mul32  11071  mul31  11072  mul4  11073  00id  11080  divass  11581  cju  11899  div4p1lem1div2  12158  xmulasslem3  12949  mulbinom2  13866  sqoddm1div8  13886  faclbnd5  13940  bcval5  13960  remim  14756  imval2  14790  sqrlem7  14888  sqrtneglem  14906  sqreulem  14999  clim2div  15529  prodfmul  15530  prodmolem3  15571  sinhval  15791  coshval  15792  absefib  15835  efieq1re  15836  muldvds1  15918  muldvds2  15919  dvdsmulc  15921  dvdsmulcr  15923  dvdstr  15931  eulerthlem2  16411  oddprmdvds  16532  ablfacrp  19584  cncrng  20531  nmoleub2lem3  24184  cnlmod  24209  itg2mulc  24817  abssinper  25582  sinasin  25944  dchrabl  26307  bposlem6  26342  bposlem9  26345  2sqlem6  26476  rpvmasum2  26565  cncvcOLD  28846  ipasslem5  29098  ipasslem11  29103  dvasin  35788  facp2  40027  fac2xp3  40088  pellexlem2  40568  jm2.25  40737  expgrowth  41842  2zrngmsgrp  45393  nn0sumshdiglemA  45853