Theorem mulass 11202

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  (class class class)co 7413  ℂcc 11112   · cmul 11119

This theorem was proved from axioms:  ax-mulass 11180

This theorem is referenced by:  mulrid  11218  mulassi  11231  mulassd  11243  mul12  11385  mul32  11386  mul31  11387  mul4  11388  00id  11395  divass  11896  cju  12214  div4p1lem1div2  12473  xmulasslem3  13271  mulbinom2  14192  sqoddm1div8  14212  faclbnd5  14264  bcval5  14284  remim  15070  imval2  15104  01sqrexlem7  15201  sqrtneglem  15219  sqreulem  15312  clim2div  15841  prodfmul  15842  prodmolem3  15883  sinhval  16103  coshval  16104  absefib  16147  efieq1re  16148  muldvds1  16230  muldvds2  16231  dvdsmulc  16233  dvdsmulcr  16235  dvdstr  16243  eulerthlem2  16721  oddprmdvds  16842  ablfacrp  19979  cncrng  21168  nmoleub2lem3  24864  cnlmod  24889  itg2mulc  25499  abssinper  26264  sinasin  26628  dchrabl  26991  bposlem6  27026  bposlem9  27029  2sqlem6  27160  rpvmasum2  27249  cncvcOLD  30101  ipasslem5  30353  ipasslem11  30358  gg-cncrng  35488  dvasin  36877  facp2  41267  fac2xp3  41328  pellexlem2  41872  jm2.25  42042  expgrowth  43398  2zrngmsgrp  46935  nn0sumshdiglemA  47394