Theorem mulcomli 11236

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  (class class class)co 7423  ℂcc 11116   · cmul 11123

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738  ax-mulcom 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  divcan1i  11977  mvllmuli  12066  recgt0ii  12139  2t3e6  12425  2t4e8  12428  nummul2c  12784  5recm6rec  12879  dec5nprm  17151  karatsuba  17168  2exp11  17174  2exp16  17175  13prm  17201  17prm  17202  19prm  17203  23prm  17204  43prm  17207  83prm  17208  139prm  17209  163prm  17210  317prm  17211  631prm  17212  1259lem1  17216  1259lem2  17217  1259lem3  17218  1259lem4  17219  1259lem5  17220  1259prm  17221  2503lem1  17222  2503lem2  17223  2503lem3  17224  2503prm  17225  4001lem1  17226  4001lem2  17227  4001lem3  17228  4001lem4  17229  4001prm  17230  pcoass  25220  efif1olem2  26745  mcubic  27049  quart1  27058  quartlem1  27059  tanatan  27121  log2ublem3  27150  log2ub  27151  bclbnd  27481  bpos1lem  27483  bposlem4  27488  bposlem5  27489  bposlem8  27492  2lgsoddprmlem3c  27613  ex-exp  30838  ex-fac  30839  ex-prmo  30847  ipasslem10  31228  siii  31242  normlem3  31501  bcsiALT  31568  dpmul1000  33255  hgt750lem2  35071  12lcm5e60  42816  60lcm7e420  42818  3exp7  42861  3lexlogpow5ineq1  42862  3lexlogpow2ineq2  42867  3lexlogpow5ineq5  42868  aks4d1p1  42884  25or6to4  43014  4t5e20  43093  235t711  43107  ex-decpmul  43108  0tie0  43117  3cubeslem3r  43459  sqrtcval2  44409  resqrtvalex  44412  inductionexd  44922  fouriersw  46986  goldrasin  47660  1t10e1p1e11  48088  fmtno5lem1  48346  fmtno5lem2  48347  257prm  48354  fmtno4prmfac  48365  fmtno4nprmfac193  48367  fmtno5faclem2  48373  139prmALT  48389  127prm  48392  41prothprmlem2  48411  2exp340mod341  48539  8exp8mod9  48542  gpg5order  48866