Theorem mulcomi 11298

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

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

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

This theorem is referenced by:  mulcomli  11299  divmul13i  12055  8th4div3  12513  numma2c  12804  nummul2c  12808  9t11e99  12888  binom2i  14261  fac3  14329  tanval2  16181  pockthi  16954  mod2xnegi  17118  decexp2  17122  decsplit1  17129  decsplit  17130  83prm  17170  dvsincos  26039  sincosq4sgn  26561  2logb9irrALT  26859  ang180lem3  26872  mcubic  26908  cubic2  26909  log2ublem2  27008  log2ublem3  27009  log2ub  27010  basellem8  27149  ppiub  27266  chtub  27274  bposlem8  27353  2lgsoddprmlem2  27471  2lgsoddprmlem3d  27475  ax5seglem7  28968  ex-ind-dvds  30493  ipdirilem  30861  siilem1  30883  bcseqi  31152  h1de2i  31585  dpmul10  32859  dpmul4  32878  signswch  34538  hgt750lem  34628  hgt750lem2  34629  problem4  35636  problem5  35637  quad3  35638  mulcomnni  41944  lcmineqlem23  42008  3lexlogpow5ineq1  42011  arearect  43176  areaquad  43177  wallispilem4  45989  dirkercncflem1  46024  fourierswlem  46151  257prm  47435  fmtno4prmfac  47446  5tcu2e40  47489  41prothprm  47493  tgoldbachlt  47690  zlmodzxzequap  48228