Theorem mulcomli 11145

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709  ax-mulcom 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  divcan1i  11890  mvllmuli  11979  recgt0ii  12053  halfthird  12389  nummul2c  12685  5recm6rec  12778  sq4e2t8  14152  cos2bnd  16146  prmo3  17003  dec5nprm  17028  karatsuba  17045  2exp6  17048  2exp8  17050  2exp11  17051  2exp16  17052  7prm  17072  13prm  17077  17prm  17078  19prm  17079  23prm  17080  43prm  17083  83prm  17084  139prm  17085  163prm  17086  317prm  17087  631prm  17088  1259lem1  17092  1259lem2  17093  1259lem3  17094  1259lem4  17095  1259lem5  17096  1259prm  17097  2503lem1  17098  2503lem2  17099  2503lem3  17100  2503prm  17101  4001lem1  17102  4001lem2  17103  4001lem3  17104  4001lem4  17105  4001prm  17106  pcoass  25001  efif1olem2  26520  mcubic  26824  quart1lem  26832  quart1  26833  quartlem1  26834  tanatan  26896  log2ublem3  26925  log2ub  26926  cht3  27150  bclbnd  27257  bpos1lem  27259  bposlem4  27264  bposlem5  27265  bposlem8  27268  2lgslem3a  27373  2lgsoddprmlem3c  27389  2lgsoddprmlem3d  27390  ex-exp  30535  ex-fac  30536  ex-prmo  30544  ipasslem10  30925  siii  30939  normlem3  31198  bcsiALT  31265  dpmul1000  32973  hgt750lem2  34812  12lcm5e60  42461  60lcm7e420  42463  420lcm8e840  42464  3exp7  42506  3lexlogpow5ineq1  42507  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1p1  42529  4t5e20  42737  235t711  42751  ex-decpmul  42752  0tie0  42761  3cubeslem3l  43132  3cubeslem3r  43133  sqrtcval2  44087  resqrtvalex  44090  inductionexd  44600  fouriersw  46677  goldrasin  47344  1t10e1p1e11  47770  fmtno5lem1  48028  fmtno5lem2  48029  257prm  48036  fmtno4prmfac  48047  fmtno4nprmfac193  48049  fmtno5faclem2  48055  139prmALT  48071  127prm  48074  mod42tp1mod8  48077  3exp4mod41  48091  41prothprmlem2  48093  2exp340mod341  48221  8exp8mod9  48224  gpg5order  48548