Theorem mulcomli 11270

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708  ax-mulcom 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  divcan1i  12011  mvllmuli  12100  recgt0ii  12174  nummul2c  12783  halfthird  12876  5recm6rec  12877  sq4e2t8  14238  cos2bnd  16224  prmo3  17079  dec5nprm  17104  karatsuba  17121  2exp6  17124  2exp8  17126  2exp11  17127  2exp16  17128  7prm  17148  13prm  17153  17prm  17154  19prm  17155  23prm  17156  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  pcoass  25057  efif1olem2  26585  mcubic  26890  quart1lem  26898  quart1  26899  quartlem1  26900  tanatan  26962  log2ublem3  26991  log2ub  26992  cht3  27216  bclbnd  27324  bpos1lem  27326  bposlem4  27331  bposlem5  27332  bposlem8  27335  2lgslem3a  27440  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  ex-exp  30469  ex-fac  30470  ex-prmo  30478  ipasslem10  30858  siii  30872  normlem3  31131  bcsiALT  31198  dpmul1000  32881  hgt750lem2  34667  12lcm5e60  42009  60lcm7e420  42011  420lcm8e840  42012  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1p1  42077  4t5e20  42326  235t711  42339  ex-decpmul  42340  0tie0  42350  3cubeslem3l  42697  3cubeslem3r  42698  sqrtcval2  43655  resqrtvalex  43658  inductionexd  44168  fouriersw  46246  1t10e1p1e11  47322  fmtno5lem1  47540  fmtno5lem2  47541  257prm  47548  fmtno4prmfac  47559  fmtno4nprmfac193  47561  fmtno5faclem2  47567  139prmALT  47583  127prm  47586  mod42tp1mod8  47589  3exp4mod41  47603  41prothprmlem2  47605  2exp340mod341  47720  8exp8mod9  47723  gpg5order  48014