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

Theorem mulcomi 10637
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 10611 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3mp2an 688 1 (𝐴 · 𝐵) = (𝐵 · 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 10589
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  mulcomli  10638  divmul13i  11389  8th4div3  11845  numma2c  12132  nummul2c  12136  9t11e99  12216  binom2i  13562  fac3  13628  tanval2  15474  pockthi  16231  mod2xnegi  16395  decexp2  16399  decsplit1  16406  decsplit  16407  83prm  16444  dvsincos  24505  sincosq4sgn  25014  2logb9irrALT  25303  ang180lem3  25316  mcubic  25352  cubic2  25353  log2ublem2  25452  log2ublem3  25453  log2ub  25454  basellem8  25592  ppiub  25707  chtub  25715  bposlem8  25794  2lgsoddprmlem2  25912  2lgsoddprmlem3d  25916  ax5seglem7  26648  ex-ind-dvds  28167  ipdirilem  28533  siilem1  28555  bcseqi  28824  h1de2i  29257  dpmul10  30498  dpmul4  30517  signswch  31730  hgt750lem  31821  hgt750lem2  31822  problem4  32808  problem5  32809  quad3  32810  arearect  39700  areaquad  39701  wallispilem4  42230  dirkercncflem1  42265  fourierswlem  42392  257prm  43600  fmtno4prmfac  43611  5tcu2e40  43657  41prothprm  43661  tgoldbachlt  43858  zlmodzxzequap  44482
  Copyright terms: Public domain W3C validator