Theorem mulcomli 11118

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

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 2121  ax-ext 2703  ax-mulcom 11067

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

This theorem is referenced by:  divcan1i  11862  mvllmuli  11951  recgt0ii  12025  halfthird  12339  nummul2c  12635  5recm6rec  12728  sq4e2t8  14103  cos2bnd  16094  prmo3  16950  dec5nprm  16975  karatsuba  16992  2exp6  16995  2exp8  16997  2exp11  16998  2exp16  16999  7prm  17019  13prm  17024  17prm  17025  19prm  17026  23prm  17027  43prm  17030  83prm  17031  139prm  17032  163prm  17033  317prm  17034  631prm  17035  1259lem1  17039  1259lem2  17040  1259lem3  17041  1259lem4  17042  1259lem5  17043  1259prm  17044  2503lem1  17045  2503lem2  17046  2503lem3  17047  2503prm  17048  4001lem1  17049  4001lem2  17050  4001lem3  17051  4001lem4  17052  4001prm  17053  pcoass  24949  efif1olem2  26477  mcubic  26782  quart1lem  26790  quart1  26791  quartlem1  26792  tanatan  26854  log2ublem3  26883  log2ub  26884  cht3  27108  bclbnd  27216  bpos1lem  27218  bposlem4  27223  bposlem5  27224  bposlem8  27227  2lgslem3a  27332  2lgsoddprmlem3c  27348  2lgsoddprmlem3d  27349  ex-exp  30425  ex-fac  30426  ex-prmo  30434  ipasslem10  30814  siii  30828  normlem3  31087  bcsiALT  31154  dpmul1000  32874  hgt750lem2  34660  12lcm5e60  42040  60lcm7e420  42042  420lcm8e840  42043  3exp7  42085  3lexlogpow5ineq1  42086  3lexlogpow2ineq2  42091  3lexlogpow5ineq5  42092  aks4d1p1  42108  4t5e20  42323  235t711  42337  ex-decpmul  42338  0tie0  42347  3cubeslem3l  42718  3cubeslem3r  42719  sqrtcval2  43674  resqrtvalex  43677  inductionexd  44187  fouriersw  46268  1t10e1p1e11  47340  fmtno5lem1  47583  fmtno5lem2  47584  257prm  47591  fmtno4prmfac  47602  fmtno4nprmfac193  47604  fmtno5faclem2  47610  139prmALT  47626  127prm  47629  mod42tp1mod8  47632  3exp4mod41  47646  41prothprmlem2  47648  2exp340mod341  47763  8exp8mod9  47766  gpg5order  48090