Theorem mulcomi 8326

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

Syntax hints:   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   · cmul 8178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-mulcom 8274

This theorem is referenced by:  mulcomli  8327  8th4div3  9507  numma2c  9805  nummul2c  9809  9t11e99  9889  binom2i  11068  fac3  11153  tanval2ap  12463  pockthi  13120  decsplit1  13190  decsplit  13191  sincosq4sgn  15913  2logb9irrALT  16059  log2ublem2  16067  log2ublem3  16068  log2ublog2  16069  2lgsoddprmlem2  16208  2lgsoddprmlem3d  16212