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

Theorem mulcomi 10252
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 10228 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3mp2an 672 1 (𝐴 · 𝐵) = (𝐵 · 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wcel 2145  (class class class)co 6796  cc 10140   · cmul 10147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10206
This theorem depends on definitions:  df-bi 197  df-an 383
This theorem is referenced by:  mulcomli  10253  divmul13i  10992  8th4div3  11459  numma2c  11765  nummul2c  11769  9t11e99  11877  9t11e99OLD  11878  binom2i  13181  fac3  13271  tanval2  15069  pockthi  15818  mod2xnegi  15982  decexp2  15986  decsplit1  15993  decsplit  15994  decsplit1OLD  15997  decsplitOLD  15998  83prm  16037  dvsincos  23964  sincosq4sgn  24474  ang180lem3  24762  mcubic  24795  cubic2  24796  log2ublem2  24895  log2ublem3  24896  log2ub  24897  basellem8  25035  ppiub  25150  chtub  25158  bposlem8  25237  2lgsoddprmlem2  25355  2lgsoddprmlem3d  25359  ax5seglem7  26036  ex-exp  27649  ex-ind-dvds  27660  ipdirilem  28024  siilem1  28046  bcseqi  28317  h1de2i  28752  dpmul10  29943  dpmul4  29962  signswch  30978  hgt750lem  31069  hgt750lem2  31070  problem4  31900  problem5  31901  quad3  31902  arearect  38325  areaquad  38326  wallispilem4  40797  dirkercncflem1  40832  fourierswlem  40959  257prm  41996  fmtno4prmfac  42007  5tcu2e40  42055  41prothprm  42059  tgoldbachlt  42227  tgoldbachltOLD  42233  zlmodzxzequap  42811
  Copyright terms: Public domain W3C validator