Theorem mulcomli 8333

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

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
mulcomli.3	⊢ (𝐴 · 𝐵) = 𝐶

Assertion

Ref	Expression
mulcomli	⊢ (𝐵 · 𝐴) = 𝐶

Proof of Theorem mulcomli

Step	Hyp	Ref	Expression
1		axi.2	. . 3 ⊢ 𝐵 ∈ ℂ
2		axi.1	. . 3 ⊢ 𝐴 ∈ ℂ
3	1, 2	mulcomi 8332	. 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵)
4		mulcomli.3	. 2 ⊢ (𝐴 · 𝐵) = 𝐶
5	3, 4	eqtri 2259	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-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220  ax-mulcom 8280

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  2t3e6  9463  nummul2c  9828  halfthird  9921  5recm6rec  9922  sq4e2t8  11076  cos2bnd  12529  dec5nprm  13195  karatsuba  13211  2exp6  13214  2exp8  13216  2exp11  13217  2exp16  13218  log2ublem3  16091  log2ublog2  16092  bclbnd  16127  2lgslem3a  16224  2lgsoddprmlem3c  16240  2lgsoddprmlem3d  16241  ex-exp  16753  ex-fac  16754