Theorem mulcomi 8332

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

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

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

This theorem is used by:  mulcomli  8333  8th4div3  9526  numma2c  9824  nummul2c  9828  9t11e99  9908  binom2i  11087  fac3  11172  tanval2ap  12482  pockthi  13139  decsplit1  13209  decsplit  13210  sincosq4sgn  15933  2logb9irrALT  16082  log2ublem2  16090  log2ublem3  16091  log2ublog2  16092  2lgsoddprmlem2  16237  2lgsoddprmlem3d  16241