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

Theorem mulcomi 10641
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 10615 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3mp2an 690 1 (𝐴 · 𝐵) = (𝐵 · 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  wcel 2107  (class class class)co 7148  cc 10527   · cmul 10534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10593
This theorem depends on definitions:  df-bi 209  df-an 399
This theorem is referenced by:  mulcomli  10642  divmul13i  11393  8th4div3  11849  numma2c  12136  nummul2c  12140  9t11e99  12220  binom2i  13566  fac3  13632  tanval2  15478  pockthi  16235  mod2xnegi  16399  decexp2  16403  decsplit1  16410  decsplit  16411  83prm  16448  dvsincos  24570  sincosq4sgn  25079  2logb9irrALT  25368  ang180lem3  25381  mcubic  25417  cubic2  25418  log2ublem2  25517  log2ublem3  25518  log2ub  25519  basellem8  25657  ppiub  25772  chtub  25780  bposlem8  25859  2lgsoddprmlem2  25977  2lgsoddprmlem3d  25981  ax5seglem7  26713  ex-ind-dvds  28232  ipdirilem  28598  siilem1  28620  bcseqi  28889  h1de2i  29322  dpmul10  30564  dpmul4  30583  signswch  31819  hgt750lem  31910  hgt750lem2  31911  problem4  32899  problem5  32900  quad3  32901  arearect  39807  areaquad  39808  wallispilem4  42338  dirkercncflem1  42373  fourierswlem  42500  257prm  43708  fmtno4prmfac  43719  5tcu2e40  43765  41prothprm  43769  tgoldbachlt  43966  zlmodzxzequap  44539
  Copyright terms: Public domain W3C validator