Theorem mulassi 11120

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

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

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

This theorem is referenced by:  8th4div3  12338  numma  12629  decbin0  12725  sq4e2t8  14103  3dec  14170  faclbnd4lem1  14197  ef01bndlem  16090  3dvdsdec  16240  3dvds2dec  16241  dec5dvds  16973  karatsuba  16992  sincos4thpi  26447  sincos6thpi  26450  ang180lem2  26745  ang180lem3  26746  asin1  26829  efiatan2  26852  2efiatan  26853  log2cnv  26879  log2ublem2  26882  log2ublem3  26883  log2ub  26884  bclbnd  27216  bposlem8  27227  2lgsoddprmlem3d  27349  ax5seglem7  28911  ipasslem10  30814  siilem1  30826  normlem0  31084  normlem9  31093  bcseqi  31095  polid2i  31132  dfdec100  32808  dpmul100  32872  dpmul1000  32874  dpexpp1  32883  dpmul4  32889  quad3  35702  iexpire  35767  mulassnni  42018  sn-1ticom  42467  sn-0tie0  42483  fourierswlem  46267  fouriersw  46268  41prothprm  47649  tgoldbachlt  47846