Theorem mulcomli 10451

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

Syntax hints:   = wceq 1507   ∈ wcel 2050  (class class class)co 6978  ℂcc 10335   · cmul 10342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750  ax-mulcom 10401

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771

This theorem is referenced by:  divcan1i  11187  mvllmuli  11276  recgt0ii  11349  nummul2c  11965  halfthird  12059  5recm6rec  12060  sq4e2t8  13380  cos2bnd  15404  prmo3  16236  dec5nprm  16261  decexp2  16270  karatsuba  16279  2exp6  16281  2exp8  16282  2exp16  16283  7prm  16303  13prm  16308  17prm  16309  19prm  16310  23prm  16311  43prm  16314  83prm  16315  139prm  16316  163prm  16317  317prm  16318  631prm  16319  1259lem1  16323  1259lem2  16324  1259lem3  16325  1259lem4  16326  1259lem5  16327  1259prm  16328  2503lem1  16329  2503lem2  16330  2503lem3  16331  2503prm  16332  4001lem1  16333  4001lem2  16334  4001lem3  16335  4001lem4  16336  4001prm  16337  pcoass  23334  efif1olem2  24831  mcubic  25129  quart1lem  25137  quart1  25138  quartlem1  25139  tanatan  25201  log2ublem3  25231  log2ub  25232  cht3  25455  bclbnd  25561  bpos1lem  25563  bposlem4  25568  bposlem5  25569  bposlem8  25572  2lgslem3a  25677  2lgsoddprmlem3c  25693  2lgsoddprmlem3d  25694  ex-exp  28010  ex-fac  28011  ex-prmo  28019  ipasslem10  28396  siii  28410  normlem3  28671  bcsiALT  28738  dpmul1000  30324  hgt750lem2  31571  235t711  38609  ex-decpmul  38610  inductionexd  39868  fouriersw  41948  1t10e1p1e11  42917  fmtno5lem1  43084  fmtno5lem2  43085  257prm  43092  fmtno4prmfac  43103  fmtno4nprmfac193  43105  fmtno5faclem2  43111  139prmALT  43128  127prm  43132  2exp11  43134  mod42tp1mod8  43136  3exp4mod41  43150  41prothprmlem2  43152  2exp340mod341  43267  8exp8mod9  43270