Theorem mulassi 10049

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 10024	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1424	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Syntax hints:   = wceq 1483   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934   · cmul 9941

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  8th4div3  11252  numma  11557  decbin0  11682  sq4e2t8  12962  3dec  13050  3decOLD  13053  faclbnd4lem1  13080  ef01bndlem  14914  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  dec5dvds  15768  karatsuba  15792  karatsubaOLD  15793  sincos4thpi  24265  sincos6thpi  24267  ang180lem2  24540  ang180lem3  24541  asin1  24621  efiatan2  24644  2efiatan  24645  log2cnv  24671  log2ublem2  24674  log2ublem3  24675  log2ub  24676  bclbnd  25005  bposlem8  25016  2lgsoddprmlem3d  25138  ax5seglem7  25815  ipasslem10  27694  siilem1  27706  normlem0  27966  normlem9  27975  bcseqi  27977  polid2i  28014  dfdec100  29576  dpmul100  29605  dpmul1000  29607  dpexpp1  29616  dpmul4  29622  quad3  31564  iexpire  31621  fourierswlem  40447  fouriersw  40448  41prothprm  41536  tgoldbachlt  41704  tgoldbachltOLD  41710