Theorem mulcomli 11220

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  ℂcc 11104   · cmul 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695  ax-mulcom 11170

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716

This theorem is referenced by:  divcan1i  11955  mvllmuli  12044  recgt0ii  12117  nummul2c  12724  halfthird  12817  5recm6rec  12818  sq4e2t8  14160  cos2bnd  16128  prmo3  16973  dec5nprm  16998  decexp2  17007  karatsuba  17016  2exp6  17019  2exp8  17021  2exp11  17022  2exp16  17023  7prm  17043  13prm  17048  17prm  17049  19prm  17050  23prm  17051  43prm  17054  83prm  17055  139prm  17056  163prm  17057  317prm  17058  631prm  17059  1259lem1  17063  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  1259prm  17068  2503lem1  17069  2503lem2  17070  2503lem3  17071  2503prm  17072  4001lem1  17073  4001lem2  17074  4001lem3  17075  4001lem4  17076  4001prm  17077  pcoass  24873  efif1olem2  26394  mcubic  26695  quart1lem  26703  quart1  26704  quartlem1  26705  tanatan  26767  log2ublem3  26796  log2ub  26797  cht3  27021  bclbnd  27129  bpos1lem  27131  bposlem4  27136  bposlem5  27137  bposlem8  27140  2lgslem3a  27245  2lgsoddprmlem3c  27261  2lgsoddprmlem3d  27262  ex-exp  30172  ex-fac  30173  ex-prmo  30181  ipasslem10  30561  siii  30575  normlem3  30834  bcsiALT  30901  dpmul1000  32532  hgt750lem2  34153  12lcm5e60  41366  60lcm7e420  41368  420lcm8e840  41369  3exp7  41411  3lexlogpow5ineq1  41412  3lexlogpow2ineq2  41417  3lexlogpow5ineq5  41418  aks4d1p1  41434  4t5e20  41692  235t711  41694  ex-decpmul  41695  3cubeslem3l  41913  3cubeslem3r  41914  sqrtcval2  42882  resqrtvalex  42885  inductionexd  43395  fouriersw  45432  1t10e1p1e11  46503  fmtno5lem1  46706  fmtno5lem2  46707  257prm  46714  fmtno4prmfac  46725  fmtno4nprmfac193  46727  fmtno5faclem2  46733  139prmALT  46749  127prm  46752  mod42tp1mod8  46755  3exp4mod41  46769  41prothprmlem2  46771  2exp340mod341  46886  8exp8mod9  46889