Theorem mulass 11117

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027   · cmul 11034

This theorem was proved from axioms:  ax-mulass 11095

This theorem is referenced by:  mulrid  11133  mulassi  11147  mulassd  11159  mul12  11302  mul32  11303  mul31  11304  mul4  11305  00id  11312  divass  11818  cju  12146  div4p1lem1div2  12423  xmulasslem3  13229  mulbinom2  14176  sqoddm1div8  14196  faclbnd5  14251  bcval5  14271  remim  15070  imval2  15104  01sqrexlem7  15201  sqrtneglem  15219  sqreulem  15313  clim2div  15845  prodfmul  15846  prodmolem3  15889  sinhval  16112  coshval  16113  absefib  16156  efieq1re  16157  muldvds1  16240  muldvds2  16241  dvdsmulc  16243  dvdsmulcr  16245  dvdstr  16254  eulerthlem2  16743  oddprmdvds  16865  ablfacrp  20034  cncrng  21368  nmoleub2lem3  25100  cnlmod  25125  itg2mulc  25732  abssinper  26503  sinasin  26871  dchrabl  27235  bposlem6  27270  bposlem9  27273  2sqlem6  27404  rpvmasum2  27493  cncvcOLD  30672  ipasslem5  30924  ipasslem11  30929  dvasin  38071  facp2  42628  pellexlem2  43275  jm2.25  43444  expgrowth  44779  2zrngmsgrp  48744  nn0sumshdiglemA  49110