Theorem mulcomli 11246

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133

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 2155  ax-ext 2734  ax-mulcom 11192

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

This theorem is used by:  divcan1i  11987  mvllmuli  12076  recgt0ii  12149  2t3e6  12435  2t4e8  12438  nummul2c  12795  5recm6rec  12890  dec5nprm  17164  karatsuba  17181  2exp11  17187  2exp16  17188  13prm  17214  17prm  17215  19prm  17216  23prm  17217  43prm  17220  83prm  17221  139prm  17222  163prm  17223  317prm  17224  631prm  17225  1259lem1  17229  1259lem2  17230  1259lem3  17231  1259lem4  17232  1259lem5  17233  1259prm  17234  2503lem1  17235  2503lem2  17236  2503lem3  17237  2503prm  17238  4001lem1  17239  4001lem2  17240  4001lem3  17241  4001lem4  17242  4001prm  17243  pcoass  25258  efif1olem2  26788  mcubic  27092  quart1  27101  quartlem1  27102  tanatan  27164  log2ublem3  27193  log2ub  27194  bclbnd  27524  bpos1lem  27526  bposlem4  27531  bposlem5  27532  bposlem8  27535  2lgsoddprmlem3c  27656  ex-exp  30938  ex-fac  30939  ex-prmo  30947  ipasslem10  31328  siii  31342  normlem3  31601  bcsiALT  31668  dpmul1000  33352  hgt750lem2  35168  12lcm5e60  42882  60lcm7e420  42884  3exp7  42927  3lexlogpow5ineq1  42928  3lexlogpow2ineq2  42933  3lexlogpow5ineq5  42934  aks4d1p1  42950  25or6to4  43080  4t5e20  43174  235t711  43188  ex-decpmul  43189  0tie0  43198  3cubeslem3r  43540  sqrtcval2  44490  resqrtvalex  44493  inductionexd  45003  fouriersw  47067  goldrasin  47755  1t10e1p1e11  48206  fmtno5lem1  48464  fmtno5lem2  48465  257prm  48472  fmtno4prmfac  48483  fmtno4nprmfac193  48485  fmtno5faclem2  48491  139prmALT  48507  127prm  48510  41prothprmlem2  48529  2exp340mod341  48657  8exp8mod9  48660  gpg5order  48984