Theorem mulcomi 11320

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

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

This theorem is used by:  mulcomli  11321  divmul13i  12081  8th4div3  12569  numma2c  12868  nummul2c  12872  9t11e99OLD  12953  binom2i  14359  tanval2  16306  pockthi  17090  mod2xnegi  17254  decsplit1  17264  decsplit  17265  83prm  17306  dvsincos  26306  sincosq4sgn  26835  2logb9irrALT  27131  ang180lem3  27144  mcubic  27180  cubic2  27181  log2ublem2  27280  log2ublem3  27281  log2ub  27282  chtub  27544  bposlem8  27623  2lgsoddprmlem2  27741  2lgsoddprmlem3d  27745  ax5seglem7  29518  ex-ind-dvds  31067  ipdirilem  31436  siilem1  31458  bcseqi  31727  h1de2i  32160  dpmul10  33507  dpmul4  33526  signswch  35236  hgt750lem  35326  hgt750lem2  35327  problem4  36519  problem5  36520  quad3  36521  mulcomnni  43130  lcmineqlem23  43194  3lexlogpow5ineq1  43197  arearect  44310  areaquad  44311  wallispilem4  47171  dirkercncflem1  47206  fourierswlem  47333  goldpolyfactor  48020  goldratmolem2  48026  257prm  48739  fmtno4prmfac  48750  5tcu2e40  48793  41prothprm  48797  tgoldbachlt  49007  zlmodzxzequap  49704