Theorem mulcomi 11182

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

Hypotheses

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

Assertion

Ref	Expression
mulcomi	⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Proof of Theorem mulcomi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcom 11154	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

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

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

This theorem is referenced by:  mulcomli  11183  divmul13i  11943  8th4div3  12402  numma2c  12695  nummul2c  12699  9t11e99  12779  binom2i  14177  fac3  14245  tanval2  16101  pockthi  16878  mod2xnegi  17042  decsplit1  17052  decsplit  17053  83prm  17093  dvsincos  25885  sincosq4sgn  26410  2logb9irrALT  26708  ang180lem3  26721  mcubic  26757  cubic2  26758  log2ublem2  26857  log2ublem3  26858  log2ub  26859  basellem8  26998  ppiub  27115  chtub  27123  bposlem8  27202  2lgsoddprmlem2  27320  2lgsoddprmlem3d  27324  ax5seglem7  28862  ex-ind-dvds  30390  ipdirilem  30758  siilem1  30780  bcseqi  31049  h1de2i  31482  dpmul10  32815  dpmul4  32834  signswch  34552  hgt750lem  34642  hgt750lem2  34643  problem4  35655  problem5  35656  quad3  35657  mulcomnni  41975  lcmineqlem23  42039  3lexlogpow5ineq1  42042  arearect  43204  areaquad  43205  wallispilem4  46066  dirkercncflem1  46101  fourierswlem  46228  257prm  47562  fmtno4prmfac  47573  5tcu2e40  47616  41prothprm  47620  tgoldbachlt  47817  zlmodzxzequap  48488