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

Theorem mulcomi 11269
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 11241 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
41, 2, 3mp2an 692 1 (𝐴 · 𝐵) = (𝐵 · 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  (class class class)co 7431  cc 11153   · cmul 11160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 11219
This theorem depends on definitions:  df-bi 207  df-an 396
This theorem is referenced by:  mulcomli  11270  divmul13i  12028  8th4div3  12486  numma2c  12779  nummul2c  12783  9t11e99  12863  binom2i  14251  fac3  14319  tanval2  16169  pockthi  16945  mod2xnegi  17109  decsplit1  17119  decsplit  17120  83prm  17160  dvsincos  26019  sincosq4sgn  26543  2logb9irrALT  26841  ang180lem3  26854  mcubic  26890  cubic2  26891  log2ublem2  26990  log2ublem3  26991  log2ub  26992  basellem8  27131  ppiub  27248  chtub  27256  bposlem8  27335  2lgsoddprmlem2  27453  2lgsoddprmlem3d  27457  ax5seglem7  28950  ex-ind-dvds  30480  ipdirilem  30848  siilem1  30870  bcseqi  31139  h1de2i  31572  dpmul10  32877  dpmul4  32896  signswch  34576  hgt750lem  34666  hgt750lem2  34667  problem4  35673  problem5  35674  quad3  35675  mulcomnni  41988  lcmineqlem23  42052  3lexlogpow5ineq1  42055  arearect  43227  areaquad  43228  wallispilem4  46083  dirkercncflem1  46118  fourierswlem  46245  257prm  47548  fmtno4prmfac  47559  5tcu2e40  47602  41prothprm  47606  tgoldbachlt  47803  zlmodzxzequap  48416
  Copyright terms: Public domain W3C validator