Theorem mulcomi 11241

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  mulcomli  11242  divmul13i  12000  8th4div3  12459  numma2c  12752  nummul2c  12756  9t11e99  12836  binom2i  14228  fac3  14296  tanval2  16149  pockthi  16925  mod2xnegi  17089  decsplit1  17099  decsplit  17100  83prm  17140  dvsincos  25935  sincosq4sgn  26460  2logb9irrALT  26758  ang180lem3  26771  mcubic  26807  cubic2  26808  log2ublem2  26907  log2ublem3  26908  log2ub  26909  basellem8  27048  ppiub  27165  chtub  27173  bposlem8  27252  2lgsoddprmlem2  27370  2lgsoddprmlem3d  27374  ax5seglem7  28860  ex-ind-dvds  30388  ipdirilem  30756  siilem1  30778  bcseqi  31047  h1de2i  31480  dpmul10  32815  dpmul4  32834  signswch  34539  hgt750lem  34629  hgt750lem2  34630  problem4  35636  problem5  35637  quad3  35638  mulcomnni  41946  lcmineqlem23  42010  3lexlogpow5ineq1  42013  arearect  43186  areaquad  43187  wallispilem4  46045  dirkercncflem1  46080  fourierswlem  46207  257prm  47523  fmtno4prmfac  47534  5tcu2e40  47577  41prothprm  47581  tgoldbachlt  47778  zlmodzxzequap  48423