Theorem mulass 11198

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  (class class class)co 7416  ℂcc 11108   · cmul 11115

This proof depends on axioms:  ax-mulass 11176

This theorem is used by:  mulrid  11216  mulassi  11230  mulassd  11242  mul12  11385  mul32  11386  mul31  11387  mul4  11388  00id  11395  divass  11900  cju  12224  div4p1lem1div2  12509  xmulasslem3  13322  mulbinom2  14270  sqoddm1div8  14290  faclbnd5  14345  bcval5  14365  remim  15179  imval2  15213  01sqrexlem7  15310  sqrtneglem  15328  sqreulem  15422  clim2div  15954  prodfmul  15955  prodmolem3  15998  sinhval  16220  coshval  16221  absefib  16264  efieq1re  16265  muldvds1  16348  muldvds2  16349  dvdsmulc  16351  dvdsmulcr  16353  dvdstr  16362  eulerthlem2  16851  oddprmdvds  16973  ablfacrp  20148  cncrng  21558  nmoleub2lem3  25289  cnlmod  25314  itg2mulc  25921  abssinper  26701  sinasin  27069  dchrabl  27433  bposlem6  27468  bposlem9  27471  2sqlem6  27602  rpvmasum2  27691  cncvcOLD  30950  ipasslem5  31202  ipasslem11  31207  dvasin  38387  facp2  42942  pellexlem2  43589  jm2.25  43758  expgrowth  45077  2zrngmsgrp  49050  nn0sumshdiglemA  49431