Theorem mulass 11132

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   · cmul 11049

This theorem was proved from axioms:  ax-mulass 11110

This theorem is referenced by:  mulrid  11148  mulassi  11161  mulassd  11173  mul12  11315  mul32  11316  mul31  11317  mul4  11318  00id  11325  divass  11831  cju  12158  div4p1lem1div2  12413  xmulasslem3  13222  mulbinom2  14164  sqoddm1div8  14184  faclbnd5  14239  bcval5  14259  remim  15059  imval2  15093  01sqrexlem7  15190  sqrtneglem  15208  sqreulem  15302  clim2div  15831  prodfmul  15832  prodmolem3  15875  sinhval  16098  coshval  16099  absefib  16142  efieq1re  16143  muldvds1  16226  muldvds2  16227  dvdsmulc  16229  dvdsmulcr  16231  dvdstr  16240  eulerthlem2  16728  oddprmdvds  16850  ablfacrp  19974  cncrng  21276  cncrngOLD  21277  nmoleub2lem3  24991  cnlmod  25016  itg2mulc  25624  abssinper  26406  sinasin  26775  dchrabl  27141  bposlem6  27176  bposlem9  27179  2sqlem6  27310  rpvmasum2  27399  cncvcOLD  30485  ipasslem5  30737  ipasslem11  30742  dvasin  37671  facp2  42104  pellexlem2  42791  jm2.25  42961  expgrowth  44297  2zrngmsgrp  48214  nn0sumshdiglemA  48581