Theorem mulcomli 10653

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

Syntax hints:   = wceq 1536   ∈ wcel 2113  (class class class)co 7159  ℂcc 10538   · cmul 10545

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796  ax-mulcom 10604

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817

This theorem is referenced by:  divcan1i  11387  mvllmuli  11476  recgt0ii  11549  nummul2c  12151  halfthird  12244  5recm6rec  12245  sq4e2t8  13565  cos2bnd  15544  prmo3  16380  dec5nprm  16405  decexp2  16414  karatsuba  16423  2exp6  16425  2exp8  16426  2exp16  16427  7prm  16447  13prm  16452  17prm  16453  19prm  16454  23prm  16455  43prm  16458  83prm  16459  139prm  16460  163prm  16461  317prm  16462  631prm  16463  1259lem1  16467  1259lem2  16468  1259lem3  16469  1259lem4  16470  1259lem5  16471  1259prm  16472  2503lem1  16473  2503lem2  16474  2503lem3  16475  2503prm  16476  4001lem1  16477  4001lem2  16478  4001lem3  16479  4001lem4  16480  4001prm  16481  pcoass  23631  efif1olem2  25130  mcubic  25428  quart1lem  25436  quart1  25437  quartlem1  25438  tanatan  25500  log2ublem3  25529  log2ub  25530  cht3  25753  bclbnd  25859  bpos1lem  25861  bposlem4  25866  bposlem5  25867  bposlem8  25870  2lgslem3a  25975  2lgsoddprmlem3c  25991  2lgsoddprmlem3d  25992  ex-exp  28232  ex-fac  28233  ex-prmo  28241  ipasslem10  28619  siii  28633  normlem3  28892  bcsiALT  28959  dpmul1000  30579  hgt750lem2  31927  235t711  39183  ex-decpmul  39184  3cubeslem3l  39289  3cubeslem3r  39290  inductionexd  40511  fouriersw  42523  1t10e1p1e11  43517  fmtno5lem1  43722  fmtno5lem2  43723  257prm  43730  fmtno4prmfac  43741  fmtno4nprmfac193  43743  fmtno5faclem2  43749  139prmALT  43766  127prm  43770  2exp11  43772  mod42tp1mod8  43774  3exp4mod41  43788  41prothprmlem2  43790  2exp340mod341  43905  8exp8mod9  43908