Theorem mulcomli 9904

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6527  ℂcc 9791   · cmul 9798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590  ax-mulcom 9857

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  divcan1i  10621  mvllmuli  10710  recgt0ii  10781  nummul2c  11398  halfthird  11520  5recm6rec  11521  sq4e2t8  12782  cos2bnd  14706  prmo3  15532  dec5nprm  15557  decexp2  15566  karatsuba  15579  karatsubaOLD  15580  2exp6  15582  2exp8  15583  2exp16  15584  7prm  15604  13prm  15610  17prm  15611  19prm  15612  23prm  15613  43prm  15616  83prm  15617  139prm  15618  163prm  15619  317prm  15620  631prm  15621  1259lem1  15625  1259lem2  15626  1259lem3  15627  1259lem4  15628  1259lem5  15629  1259prm  15630  2503lem1  15631  2503lem2  15632  2503lem3  15633  2503prm  15634  4001lem1  15635  4001lem2  15636  4001lem3  15637  4001lem4  15638  4001prm  15639  pcoass  22580  efif1olem2  24038  mcubic  24319  quart1lem  24327  quart1  24328  quartlem1  24329  tanatan  24391  log2ublem3  24420  log2ub  24421  cht3  24644  bclbnd  24750  bpos1lem  24752  bposlem4  24757  bposlem5  24758  bposlem8  24761  2lgslem3a  24866  2lgsoddprmlem3c  24882  2lgsoddprmlem3d  24883  ex-fac  26494  ex-prmo  26502  ipasslem10  26872  siii  26886  normlem3  27147  bcsiALT  27214  inductionexd  37267  fouriersw  38918  1t10e1p1e11  39732  1t10e1p1e11OLD  39733  fmtno5lem1  39798  fmtno5lem2  39799  257prm  39806  fmtno4prmfac  39817  fmtno4nprmfac193  39819  fmtno5faclem2  39825  139prmALT  39844  127prm  39848  2exp11  39850  mod42tp1mod8  39852  3exp4mod41  39866  41prothprmlem2  39868