Theorem mulass 11228

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138   · cmul 11145

This theorem was proved from axioms:  ax-mulass 11206

This theorem is referenced by:  mulrid  11244  mulassi  11257  mulassd  11269  mul12  11411  mul32  11412  mul31  11413  mul4  11414  00id  11421  divass  11923  cju  12241  div4p1lem1div2  12500  xmulasslem3  13300  mulbinom2  14221  sqoddm1div8  14241  faclbnd5  14293  bcval5  14313  remim  15100  imval2  15134  01sqrexlem7  15231  sqrtneglem  15249  sqreulem  15342  clim2div  15871  prodfmul  15872  prodmolem3  15913  sinhval  16134  coshval  16135  absefib  16178  efieq1re  16179  muldvds1  16261  muldvds2  16262  dvdsmulc  16264  dvdsmulcr  16266  dvdstr  16274  eulerthlem2  16754  oddprmdvds  16875  ablfacrp  20035  cncrng  21333  cncrngOLD  21334  nmoleub2lem3  25086  cnlmod  25111  itg2mulc  25721  abssinper  26500  sinasin  26866  dchrabl  27232  bposlem6  27267  bposlem9  27270  2sqlem6  27401  rpvmasum2  27490  cncvcOLD  30465  ipasslem5  30717  ipasslem11  30722  dvasin  37305  facp2  41743  fac2xp3  41822  pellexlem2  42389  jm2.25  42559  expgrowth  43911  2zrngmsgrp  47498  nn0sumshdiglemA  47875