Theorem mulcomi 8339

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 8315	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 430	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184   · cmul 8191

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8287

This theorem is used by:  mulcomli  8340  8th4div3  9536  numma2c  9839  nummul2c  9843  9t11e99  9923  binom2i  11107  fac3  11193  tanval2ap  12506  pockthi  13167  mod2xnegi  13228  decsplit1  13238  decsplit  13239  83prm  13267  sincosq4sgn  16068  2logb9irrALT  16222  log2ublem2  16234  log2ublem3  16235  log2ublog2  16236  chtqub  16308  bposlem8  16330  2lgsoddprmlem2  16442  2lgsoddprmlem3d  16446