Theorem mulcomi 11222

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 11196	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 · 𝐵) = (𝐵 · 𝐴)

Syntax hints:   = wceq 1542   ∈ wcel 2107  (class class class)co 7409  ℂcc 11108   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11174

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  mulcomli  11223  divmul13i  11975  8th4div3  12432  numma2c  12723  nummul2c  12727  9t11e99  12807  binom2i  14176  fac3  14240  tanval2  16076  pockthi  16840  mod2xnegi  17004  decexp2  17008  decsplit1  17015  decsplit  17016  83prm  17056  dvsincos  25498  sincosq4sgn  26011  2logb9irrALT  26303  ang180lem3  26316  mcubic  26352  cubic2  26353  log2ublem2  26452  log2ublem3  26453  log2ub  26454  basellem8  26592  ppiub  26707  chtub  26715  bposlem8  26794  2lgsoddprmlem2  26912  2lgsoddprmlem3d  26916  ax5seglem7  28193  ex-ind-dvds  29714  ipdirilem  30082  siilem1  30104  bcseqi  30373  h1de2i  30806  dpmul10  32061  dpmul4  32080  signswch  33572  hgt750lem  33663  hgt750lem2  33664  problem4  34653  problem5  34654  quad3  34655  mulcomnni  40853  lcmineqlem23  40916  3lexlogpow5ineq1  40919  arearect  41964  areaquad  41965  wallispilem4  44784  dirkercncflem1  44819  fourierswlem  44946  257prm  46229  fmtno4prmfac  46240  5tcu2e40  46283  41prothprm  46287  tgoldbachlt  46484  zlmodzxzequap  47180