Theorem mulcomli 10890

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 10889	. 2 ⊢ (𝐵 · 𝐴) = (𝐴 · 𝐵)
4		mulcomli.3	. 2 ⊢ (𝐴 · 𝐵) = 𝐶
5	3, 4	eqtri 2767	1 ⊢ (𝐵 · 𝐴) = 𝐶

Syntax hints:   = wceq 1543   ∈ wcel 2112  (class class class)co 7252  ℂcc 10775   · cmul 10782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2122  ax-ext 2710  ax-mulcom 10841

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2731

This theorem is referenced by:  divcan1i  11624  mvllmuli  11713  recgt0ii  11786  nummul2c  12391  halfthird  12484  5recm6rec  12485  sq4e2t8  13819  cos2bnd  15800  prmo3  16645  dec5nprm  16670  decexp2  16679  karatsuba  16688  2exp6  16691  2exp8  16693  2exp11  16694  2exp16  16695  7prm  16715  13prm  16720  17prm  16721  19prm  16722  23prm  16723  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem1  16735  1259lem2  16736  1259lem3  16737  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem1  16741  2503lem2  16742  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  pcoass  24068  efif1olem2  25579  mcubic  25877  quart1lem  25885  quart1  25886  quartlem1  25887  tanatan  25949  log2ublem3  25978  log2ub  25979  cht3  26202  bclbnd  26308  bpos1lem  26310  bposlem4  26315  bposlem5  26316  bposlem8  26319  2lgslem3a  26424  2lgsoddprmlem3c  26440  2lgsoddprmlem3d  26441  ex-exp  28690  ex-fac  28691  ex-prmo  28699  ipasslem10  29077  siii  29091  normlem3  29350  bcsiALT  29417  dpmul1000  31050  hgt750lem2  32507  12lcm5e60  39923  60lcm7e420  39925  420lcm8e840  39926  3exp7  39968  3lexlogpow5ineq1  39969  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  aks4d1p1  39990  235t711  40212  ex-decpmul  40213  3cubeslem3l  40396  3cubeslem3r  40397  sqrtcval2  41111  resqrtvalex  41114  inductionexd  41627  fouriersw  43635  1t10e1p1e11  44663  fmtno5lem1  44866  fmtno5lem2  44867  257prm  44874  fmtno4prmfac  44885  fmtno4nprmfac193  44887  fmtno5faclem2  44893  139prmALT  44909  127prm  44912  mod42tp1mod8  44915  3exp4mod41  44929  41prothprmlem2  44931  2exp340mod341  45046  8exp8mod9  45049