Theorem mulcomi 11235

Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ

Assertion

Ref	Expression
mulcomi	⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Proof of Theorem mulcomi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		mulcom 11204	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 705	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-mulcom 11182

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mulcomli  11236  divmul13i  11994  8th4div3  12482  numma2c  12780  nummul2c  12784  9t11e99OLD  12865  binom2i  14268  tanval2  16214  pockthi  16992  mod2xnegi  17156  decsplit1  17166  decsplit  17167  83prm  17208  dvsincos  26177  sincosq4sgn  26703  2logb9irrALT  27000  ang180lem3  27013  mcubic  27049  cubic2  27050  log2ublem2  27149  log2ublem3  27150  log2ub  27151  chtub  27413  bposlem8  27492  2lgsoddprmlem2  27610  2lgsoddprmlem3d  27614  ax5seglem7  29322  ex-ind-dvds  30849  ipdirilem  31218  siilem1  31240  bcseqi  31509  h1de2i  31942  dpmul10  33251  dpmul4  33270  signswch  34980  hgt750lem  35070  hgt750lem2  35071  problem4  36181  problem5  36182  quad3  36183  mulcomnni  42795  lcmineqlem23  42859  3lexlogpow5ineq1  42862  arearect  43983  areaquad  43984  wallispilem4  46823  dirkercncflem1  46858  fourierswlem  46985  goldratmolem2  47664  257prm  48354  fmtno4prmfac  48365  5tcu2e40  48408  41prothprm  48412  tgoldbachlt  48622  zlmodzxzequap  49320  crosspalti  50689  crossp3i  50690