Theorem mulcomli 8340

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 8339	. 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 6088  ℂcc 8184   · cmul 8191

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 8287

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

This theorem is used by:  2t3e6  9472  2t4e8  9475  nummul2c  9843  halfthird  9936  5recm6rec  9937  sq4e2t8  11096  cos2bnd  12553  dec5nprm  13223  karatsuba  13240  2exp6  13243  2exp8  13245  2exp11  13246  2exp16  13247  13prm  13260  17prm  13261  19prm  13262  23prm  13263  43prm  13266  83prm  13267  139prm  13268  163prm  13269  317prm  13270  631prm  13271  1259lem1  13272  1259lem2  13273  1259lem3  13274  1259lem4  13275  1259lem5  13276  1259prm  13277  log2ublem3  16235  log2ublog2  16236  bclbnd  16319  bpos1lem  16321  bposlem4  16326  bposlem5  16327  bposlem8  16330  2lgslem3a  16429  2lgsoddprmlem3c  16445  2lgsoddprmlem3d  16446  ex-exp  16958  ex-fac  16959