Theorem mulcomli 10047

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

Syntax hints:   = wceq 1483   ∈ wcel 1990  (class class class)co 6650  ℂcc 9934   · cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602  ax-mulcom 10000

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  divcan1i  10769  mvllmuli  10858  recgt0ii  10929  nummul2c  11563  halfthird  11685  5recm6rec  11686  sq4e2t8  12962  cos2bnd  14918  prmo3  15745  dec5nprm  15770  decexp2  15779  karatsuba  15792  karatsubaOLD  15793  2exp6  15795  2exp8  15796  2exp16  15797  7prm  15817  13prm  15823  17prm  15824  19prm  15825  23prm  15826  43prm  15829  83prm  15830  139prm  15831  163prm  15832  317prm  15833  631prm  15834  1259lem1  15838  1259lem2  15839  1259lem3  15840  1259lem4  15841  1259lem5  15842  1259prm  15843  2503lem1  15844  2503lem2  15845  2503lem3  15846  2503prm  15847  4001lem1  15848  4001lem2  15849  4001lem3  15850  4001lem4  15851  4001prm  15852  pcoass  22824  efif1olem2  24289  mcubic  24574  quart1lem  24582  quart1  24583  quartlem1  24584  tanatan  24646  log2ublem3  24675  log2ub  24676  cht3  24899  bclbnd  25005  bpos1lem  25007  bposlem4  25012  bposlem5  25013  bposlem8  25016  2lgslem3a  25121  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  ex-fac  27308  ex-prmo  27316  ipasslem10  27694  siii  27708  normlem3  27969  bcsiALT  28036  dpmul1000  29607  hgt750lem2  30730  inductionexd  38453  fouriersw  40448  1t10e1p1e11  41319  1t10e1p1e11OLD  41320  fmtno5lem1  41465  fmtno5lem2  41466  257prm  41473  fmtno4prmfac  41484  fmtno4nprmfac193  41486  fmtno5faclem2  41492  139prmALT  41511  127prm  41515  2exp11  41517  mod42tp1mod8  41519  3exp4mod41  41533  41prothprmlem2  41535