Theorem mulcomli 11242

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

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 2707  ax-mulcom 11191

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

This theorem is referenced by:  divcan1i  11983  mvllmuli  12072  recgt0ii  12146  halfthird  12460  nummul2c  12756  5recm6rec  12849  sq4e2t8  14215  cos2bnd  16204  prmo3  17059  dec5nprm  17084  karatsuba  17101  2exp6  17104  2exp8  17106  2exp11  17107  2exp16  17108  7prm  17128  13prm  17133  17prm  17134  19prm  17135  23prm  17136  43prm  17139  83prm  17140  139prm  17141  163prm  17142  317prm  17143  631prm  17144  1259lem1  17148  1259lem2  17149  1259lem3  17150  1259lem4  17151  1259lem5  17152  1259prm  17153  2503lem1  17154  2503lem2  17155  2503lem3  17156  2503prm  17157  4001lem1  17158  4001lem2  17159  4001lem3  17160  4001lem4  17161  4001prm  17162  pcoass  24973  efif1olem2  26502  mcubic  26807  quart1lem  26815  quart1  26816  quartlem1  26817  tanatan  26879  log2ublem3  26908  log2ub  26909  cht3  27133  bclbnd  27241  bpos1lem  27243  bposlem4  27248  bposlem5  27249  bposlem8  27252  2lgslem3a  27357  2lgsoddprmlem3c  27373  2lgsoddprmlem3d  27374  ex-exp  30377  ex-fac  30378  ex-prmo  30386  ipasslem10  30766  siii  30780  normlem3  31039  bcsiALT  31106  dpmul1000  32819  hgt750lem2  34630  12lcm5e60  41967  60lcm7e420  41969  420lcm8e840  41970  3exp7  42012  3lexlogpow5ineq1  42013  3lexlogpow2ineq2  42018  3lexlogpow5ineq5  42019  aks4d1p1  42035  4t5e20  42288  235t711  42301  ex-decpmul  42302  0tie0  42311  3cubeslem3l  42656  3cubeslem3r  42657  sqrtcval2  43613  resqrtvalex  43616  inductionexd  44126  fouriersw  46208  1t10e1p1e11  47287  fmtno5lem1  47515  fmtno5lem2  47516  257prm  47523  fmtno4prmfac  47534  fmtno4nprmfac193  47536  fmtno5faclem2  47542  139prmALT  47558  127prm  47561  mod42tp1mod8  47564  3exp4mod41  47578  41prothprmlem2  47580  2exp340mod341  47695  8exp8mod9  47698  gpg5order  48012