Theorem mulcomli 11345

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735  ax-mulcom 11291

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

This theorem is used by:  divcan1i  12088  mvllmuli  12177  recgt0ii  12250  2t3e6  12536  2t4e8  12539  nummul2c  12896  5recm6rec  12991  dec5nprm  17273  karatsuba  17290  2exp11  17296  2exp16  17297  13prm  17323  17prm  17324  19prm  17325  23prm  17326  43prm  17329  83prm  17330  139prm  17331  163prm  17332  317prm  17333  631prm  17334  1259lem1  17338  1259lem2  17339  1259lem3  17340  1259lem4  17341  1259lem5  17342  1259prm  17343  2503lem1  17344  2503lem2  17345  2503lem3  17346  2503prm  17347  4001lem1  17348  4001lem2  17349  4001lem3  17350  4001lem4  17351  4001prm  17352  pcoass  25375  efif1olem2  26901  mcubic  27205  quart1  27214  quartlem1  27215  tanatan  27277  log2ublem3  27306  log2ub  27307  bclbnd  27637  bpos1lem  27639  bposlem4  27644  bposlem5  27645  bposlem8  27648  2lgsoddprmlem3c  27769  ex-exp  31081  ex-fac  31082  ex-prmo  31090  ipasslem10  31471  siii  31485  normlem3  31744  bcsiALT  31811  dpmul1000  33535  hgt750lem2  35351  12lcm5e60  43250  60lcm7e420  43252  3exp7  43295  3lexlogpow5ineq1  43296  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1p1  43318  25or6to4  43448  4t5e20  43541  235t711  43555  ex-decpmul  43556  0tie0  43565  3cubeslem3r  43890  sqrtcval2  44834  resqrtvalex  44837  inductionexd  45347  fouriersw  47446  goldrasin  48134  1t10e1p1e11  48585  fmtno5lem1  48843  fmtno5lem2  48844  257prm  48851  fmtno4prmfac  48862  fmtno4nprmfac193  48864  fmtno5faclem2  48870  139prmALT  48886  127prm  48889  41prothprmlem2  48908  2exp340mod341  49036  8exp8mod9  49039  gpg5order  49363