Theorem mulcomli 11173

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   · cmul 11065

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702  ax-mulcom 11124

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  divcan1i  11908  mvllmuli  11997  recgt0ii  12070  nummul2c  12677  halfthird  12770  5recm6rec  12771  sq4e2t8  14113  cos2bnd  16081  prmo3  16924  dec5nprm  16949  decexp2  16958  karatsuba  16967  2exp6  16970  2exp8  16972  2exp11  16973  2exp16  16974  7prm  16994  13prm  16999  17prm  17000  19prm  17001  23prm  17002  43prm  17005  83prm  17006  139prm  17007  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  1259lem5  17018  1259prm  17019  2503lem1  17020  2503lem2  17021  2503lem3  17022  2503prm  17023  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  4001prm  17028  pcoass  24424  efif1olem2  25936  mcubic  26234  quart1lem  26242  quart1  26243  quartlem1  26244  tanatan  26306  log2ublem3  26335  log2ub  26336  cht3  26559  bclbnd  26665  bpos1lem  26667  bposlem4  26672  bposlem5  26673  bposlem8  26676  2lgslem3a  26781  2lgsoddprmlem3c  26797  2lgsoddprmlem3d  26798  ex-exp  29457  ex-fac  29458  ex-prmo  29466  ipasslem10  29844  siii  29858  normlem3  30117  bcsiALT  30184  dpmul1000  31825  hgt750lem2  33354  12lcm5e60  40538  60lcm7e420  40540  420lcm8e840  40541  3exp7  40583  3lexlogpow5ineq1  40584  3lexlogpow2ineq2  40589  3lexlogpow5ineq5  40590  aks4d1p1  40606  235t711  40863  ex-decpmul  40864  3cubeslem3l  41067  3cubeslem3r  41068  sqrtcval2  42036  resqrtvalex  42039  inductionexd  42549  fouriersw  44592  1t10e1p1e11  45662  fmtno5lem1  45865  fmtno5lem2  45866  257prm  45873  fmtno4prmfac  45884  fmtno4nprmfac193  45886  fmtno5faclem2  45892  139prmALT  45908  127prm  45911  mod42tp1mod8  45914  3exp4mod41  45928  41prothprmlem2  45930  2exp340mod341  46045  8exp8mod9  46048