Theorem mulass 9903

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

This theorem was proved from axioms:  ax-mulass 9881

This theorem is referenced by:  mulid1  9916  mulassi  9928  mulassd  9942  mul12  10081  mul32  10082  mul31  10083  mul4  10084  00id  10090  divass  10582  cju  10893  div4p1lem1div2  11164  xmulasslem3  11988  mulbinom2  12846  sqoddm1div8  12890  faclbnd5  12947  bcval5  12967  remim  13705  imval2  13739  sqrlem7  13837  sqrtneglem  13855  sqreulem  13947  clim2div  14460  prodfmul  14461  prodmolem3  14502  sinhval  14723  coshval  14724  absefib  14767  efieq1re  14768  muldvds1  14844  muldvds2  14845  dvdsmulc  14847  dvdsmulcr  14849  dvdstr  14856  eulerthlem2  15325  oddprmdvds  15445  ablfacrp  18288  cncrng  19586  nmoleub2lem3  22723  cnlmod  22748  itg2mulc  23320  abssinper  24074  sinasin  24416  dchrabl  24779  bposlem6  24814  bposlem9  24817  lgsdir  24857  lgsdi  24859  2sqlem6  24948  rpvmasum2  25001  cncvcOLD  26822  ipasslem5  27074  ipasslem11  27079  dvasin  32666  pellexlem2  36412  jm2.25  36584  expgrowth  37556  2zrngmsgrp  41737  nn0sumshdiglemA  42211