Theorem mulassi 11301

Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
mulassi	⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Proof of Theorem mulassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		mulass 11272	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1461	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Syntax hints:   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11250

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  8th4div3  12513  numma  12802  decbin0  12898  sq4e2t8  14248  3dec  14315  faclbnd4lem1  14342  ef01bndlem  16232  3dvdsdec  16380  3dvds2dec  16381  dec5dvds  17111  karatsuba  17131  sincos4thpi  26573  sincos6thpi  26576  ang180lem2  26871  ang180lem3  26872  asin1  26955  efiatan2  26978  2efiatan  26979  log2cnv  27005  log2ublem2  27008  log2ublem3  27009  log2ub  27010  bclbnd  27342  bposlem8  27353  2lgsoddprmlem3d  27475  ax5seglem7  28968  ipasslem10  30871  siilem1  30883  normlem0  31141  normlem9  31150  bcseqi  31152  polid2i  31189  dfdec100  32834  dpmul100  32861  dpmul1000  32863  dpexpp1  32872  dpmul4  32878  quad3  35638  iexpire  35697  mulassnni  41943  sn-1ticom  42410  sn-0tie0  42415  sn-inelr  42443  fourierswlem  46151  fouriersw  46152  41prothprm  47493  tgoldbachlt  47690