MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulcomi Structured version   Visualization version   GIF version

Theorem mulcomi 9990
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
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 mulcom 9966 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3mp2an 707 1 (𝐴 · 𝐵) = (𝐵 · 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  (class class class)co 6604  cc 9878   · cmul 9885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9944
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  mulcomli  9991  divmul13i  10730  8th4div3  11196  numma2c  11503  nummul2c  11507  9t11e99  11615  9t11e99OLD  11616  binom2i  12914  fac3  13007  tanval2  14788  pockthi  15535  mod2xnegi  15699  decexp2  15703  decsplit1  15710  decsplit  15711  decsplit1OLD  15714  decsplitOLD  15715  83prm  15754  dvsincos  23648  sincosq4sgn  24157  ang180lem3  24441  mcubic  24474  cubic2  24475  log2ublem2  24574  log2ublem3  24575  log2ub  24576  basellem8  24714  ppiub  24829  chtub  24837  bposlem8  24916  2lgsoddprmlem2  25034  2lgsoddprmlem3d  25038  ax5seglem7  25715  ex-exp  27161  ex-ind-dvds  27172  ipdirilem  27530  siilem1  27552  bcseqi  27823  h1de2i  28258  signswch  30415  problem4  31267  problem5  31268  quad3  31269  arearect  37279  areaquad  37280  wallispilem4  39589  dirkercncflem1  39624  fourierswlem  39751  257prm  40769  fmtno4prmfac  40780  5tcu2e40  40828  41prothprm  40832  tgoldbachlt  40988  tgoldbachltOLD  40995  zlmodzxzequap  41573
  Copyright terms: Public domain W3C validator