Theorem mulcomli 11141

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708  ax-mulcom 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  divcan1i  11885  mvllmuli  11974  recgt0ii  12048  halfthird  12362  nummul2c  12657  5recm6rec  12750  sq4e2t8  14122  cos2bnd  16113  prmo3  16969  dec5nprm  16994  karatsuba  17011  2exp6  17014  2exp8  17016  2exp11  17017  2exp16  17018  7prm  17038  13prm  17043  17prm  17044  19prm  17045  23prm  17046  43prm  17049  83prm  17050  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  1259lem5  17062  1259prm  17063  2503lem1  17064  2503lem2  17065  2503lem3  17066  2503prm  17067  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  pcoass  24980  efif1olem2  26508  mcubic  26813  quart1lem  26821  quart1  26822  quartlem1  26823  tanatan  26885  log2ublem3  26914  log2ub  26915  cht3  27139  bclbnd  27247  bpos1lem  27249  bposlem4  27254  bposlem5  27255  bposlem8  27258  2lgslem3a  27363  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  ex-exp  30525  ex-fac  30526  ex-prmo  30534  ipasslem10  30914  siii  30928  normlem3  31187  bcsiALT  31254  dpmul1000  32980  hgt750lem2  34809  12lcm5e60  42258  60lcm7e420  42260  420lcm8e840  42261  3exp7  42303  3lexlogpow5ineq1  42304  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1p1  42326  4t5e20  42542  235t711  42556  ex-decpmul  42557  0tie0  42566  3cubeslem3l  42924  3cubeslem3r  42925  sqrtcval2  43879  resqrtvalex  43882  inductionexd  44392  fouriersw  46471  1t10e1p1e11  47552  fmtno5lem1  47795  fmtno5lem2  47796  257prm  47803  fmtno4prmfac  47814  fmtno4nprmfac193  47816  fmtno5faclem2  47822  139prmALT  47838  127prm  47841  mod42tp1mod8  47844  3exp4mod41  47858  41prothprmlem2  47860  2exp340mod341  47975  8exp8mod9  47978  gpg5order  48302