Theorem mulcomli 11321

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201   · cmul 11208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732  ax-mulcom 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  divcan1i  12064  mvllmuli  12153  recgt0ii  12226  2t3e6  12512  2t4e8  12515  nummul2c  12872  5recm6rec  12967  dec5nprm  17249  karatsuba  17266  2exp11  17272  2exp16  17273  13prm  17299  17prm  17300  19prm  17301  23prm  17302  43prm  17305  83prm  17306  139prm  17307  163prm  17308  317prm  17309  631prm  17310  1259lem1  17314  1259lem2  17315  1259lem3  17316  1259lem4  17317  1259lem5  17318  1259prm  17319  2503lem1  17320  2503lem2  17321  2503lem3  17322  2503prm  17323  4001lem1  17324  4001lem2  17325  4001lem3  17326  4001lem4  17327  4001prm  17328  pcoass  25350  efif1olem2  26876  mcubic  27180  quart1  27189  quartlem1  27190  tanatan  27252  log2ublem3  27281  log2ub  27282  bclbnd  27612  bpos1lem  27614  bposlem4  27619  bposlem5  27620  bposlem8  27623  2lgsoddprmlem3c  27744  ex-exp  31056  ex-fac  31057  ex-prmo  31065  ipasslem10  31446  siii  31460  normlem3  31719  bcsiALT  31786  dpmul1000  33511  hgt750lem2  35327  12lcm5e60  43151  60lcm7e420  43153  3exp7  43196  3lexlogpow5ineq1  43197  3lexlogpow2ineq2  43202  3lexlogpow5ineq5  43203  aks4d1p1  43219  25or6to4  43349  4t5e20  43441  235t711  43455  ex-decpmul  43456  0tie0  43465  3cubeslem3r  43790  sqrtcval2  44735  resqrtvalex  44738  inductionexd  45248  fouriersw  47334  goldrasin  48022  1t10e1p1e11  48473  fmtno5lem1  48731  fmtno5lem2  48732  257prm  48739  fmtno4prmfac  48750  fmtno4nprmfac193  48752  fmtno5faclem2  48758  139prmALT  48774  127prm  48777  41prothprmlem2  48796  2exp340mod341  48924  8exp8mod9  48927  gpg5order  49251