Theorem mulcomi 8333

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

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

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

This theorem is used by:  mulcomli  8334  8th4div3  9529  numma2c  9832  nummul2c  9836  9t11e99  9916  binom2i  11100  fac3  11186  tanval2ap  12499  pockthi  13160  mod2xnegi  13221  decsplit1  13231  decsplit  13232  83prm  13260  sincosq4sgn  16022  2logb9irrALT  16176  log2ublem2  16188  log2ublem3  16189  log2ublog2  16190  chtqub  16262  bposlem8  16284  2lgsoddprmlem2  16396  2lgsoddprmlem3d  16400