Theorem mulass 11198

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

This theorem was proved from axioms:  ax-mulass 11176

This theorem is referenced by:  mulrid  11212  mulassi  11225  mulassd  11237  mul12  11379  mul32  11380  mul31  11381  mul4  11382  00id  11389  divass  11890  cju  12208  div4p1lem1div2  12467  xmulasslem3  13265  mulbinom2  14186  sqoddm1div8  14206  faclbnd5  14258  bcval5  14278  remim  15064  imval2  15098  01sqrexlem7  15195  sqrtneglem  15213  sqreulem  15306  clim2div  15835  prodfmul  15836  prodmolem3  15877  sinhval  16097  coshval  16098  absefib  16141  efieq1re  16142  muldvds1  16224  muldvds2  16225  dvdsmulc  16227  dvdsmulcr  16229  dvdstr  16237  eulerthlem2  16715  oddprmdvds  16836  ablfacrp  19936  cncrng  20966  nmoleub2lem3  24631  cnlmod  24656  itg2mulc  25265  abssinper  26030  sinasin  26394  dchrabl  26757  bposlem6  26792  bposlem9  26795  2sqlem6  26926  rpvmasum2  27015  cncvcOLD  29836  ipasslem5  30088  ipasslem11  30093  dvasin  36572  facp2  40959  fac2xp3  41020  pellexlem2  41568  jm2.25  41738  expgrowth  43094  2zrngmsgrp  46845  nn0sumshdiglemA  47305