Theorem mulcomli 10259

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

Syntax hints:   = wceq 1632   ∈ wcel 2139  (class class class)co 6814  ℂcc 10146   · cmul 10153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740  ax-mulcom 10212

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  divcan1i  10981  mvllmuli  11070  recgt0ii  11141  nummul2c  11775  halfthird  11897  5recm6rec  11898  sq4e2t8  13176  cos2bnd  15137  prmo3  15967  dec5nprm  15992  decexp2  16001  karatsuba  16014  karatsubaOLD  16015  2exp6  16017  2exp8  16018  2exp16  16019  7prm  16039  13prm  16045  17prm  16046  19prm  16047  23prm  16048  43prm  16051  83prm  16052  139prm  16053  163prm  16054  317prm  16055  631prm  16056  1259lem1  16060  1259lem2  16061  1259lem3  16062  1259lem4  16063  1259lem5  16064  1259prm  16065  2503lem1  16066  2503lem2  16067  2503lem3  16068  2503prm  16069  4001lem1  16070  4001lem2  16071  4001lem3  16072  4001lem4  16073  4001prm  16074  pcoass  23044  efif1olem2  24509  mcubic  24794  quart1lem  24802  quart1  24803  quartlem1  24804  tanatan  24866  log2ublem3  24895  log2ub  24896  cht3  25119  bclbnd  25225  bpos1lem  25227  bposlem4  25232  bposlem5  25233  bposlem8  25236  2lgslem3a  25341  2lgsoddprmlem3c  25357  2lgsoddprmlem3d  25358  ex-fac  27640  ex-prmo  27648  ipasslem10  28024  siii  28038  normlem3  28299  bcsiALT  28366  dpmul1000  29937  hgt750lem2  31060  inductionexd  38973  fouriersw  40969  1t10e1p1e11  41847  1t10e1p1e11OLD  41848  fmtno5lem1  41993  fmtno5lem2  41994  257prm  42001  fmtno4prmfac  42012  fmtno4nprmfac193  42014  fmtno5faclem2  42020  139prmALT  42039  127prm  42043  2exp11  42045  mod42tp1mod8  42047  3exp4mod41  42061  41prothprmlem2  42063