Theorem mulcomli 10639

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770  ax-mulcom 10590

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  divcan1i  11373  mvllmuli  11462  recgt0ii  11535  nummul2c  12136  halfthird  12229  5recm6rec  12230  sq4e2t8  13558  cos2bnd  15533  prmo3  16367  dec5nprm  16392  decexp2  16401  karatsuba  16410  2exp6  16413  2exp8  16415  2exp16  16416  7prm  16436  13prm  16441  17prm  16442  19prm  16443  23prm  16444  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  pcoass  23629  efif1olem2  25135  mcubic  25433  quart1lem  25441  quart1  25442  quartlem1  25443  tanatan  25505  log2ublem3  25534  log2ub  25535  cht3  25758  bclbnd  25864  bpos1lem  25866  bposlem4  25871  bposlem5  25872  bposlem8  25875  2lgslem3a  25980  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  ex-exp  28235  ex-fac  28236  ex-prmo  28244  ipasslem10  28622  siii  28636  normlem3  28895  bcsiALT  28962  dpmul1000  30601  hgt750lem2  32033  12lcm5e60  39296  60lcm7e420  39298  420lcm8e840  39299  3lexlogpow5ineq1  39341  235t711  39485  ex-decpmul  39486  3cubeslem3l  39627  3cubeslem3r  39628  sqrtcval2  40342  resqrtvalex  40345  inductionexd  40858  fouriersw  42873  1t10e1p1e11  43867  fmtno5lem1  44070  fmtno5lem2  44071  257prm  44078  fmtno4prmfac  44089  fmtno4nprmfac193  44091  fmtno5faclem2  44097  139prmALT  44113  127prm  44116  2exp11  44118  mod42tp1mod8  44120  3exp4mod41  44134  41prothprmlem2  44136  2exp340mod341  44251  8exp8mod9  44254