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

Theorem mulcomli 10160
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1 𝐴 ∈ ℂ
axi.2 𝐵 ∈ ℂ
mulcomli.3 (𝐴 · 𝐵) = 𝐶
Assertion
Ref Expression
mulcomli (𝐵 · 𝐴) = 𝐶

Proof of Theorem mulcomli
StepHypRef Expression
1 axi.2 . . 3 𝐵 ∈ ℂ
2 axi.1 . . 3 𝐴 ∈ ℂ
31, 2mulcomi 10159 . 2 (𝐵 · 𝐴) = (𝐴 · 𝐵)
4 mulcomli.3 . 2 (𝐴 · 𝐵) = 𝐶
53, 4eqtri 2746 1 (𝐵 · 𝐴) = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1596  wcel 2103  (class class class)co 6765  cc 10047   · cmul 10054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-ext 2704  ax-mulcom 10113
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1818  df-cleq 2717
This theorem is referenced by:  divcan1i  10882  mvllmuli  10971  recgt0ii  11042  nummul2c  11676  halfthird  11798  5recm6rec  11799  sq4e2t8  13077  cos2bnd  15038  prmo3  15868  dec5nprm  15893  decexp2  15902  karatsuba  15915  karatsubaOLD  15916  2exp6  15918  2exp8  15919  2exp16  15920  7prm  15940  13prm  15946  17prm  15947  19prm  15948  23prm  15949  43prm  15952  83prm  15953  139prm  15954  163prm  15955  317prm  15956  631prm  15957  1259lem1  15961  1259lem2  15962  1259lem3  15963  1259lem4  15964  1259lem5  15965  1259prm  15966  2503lem1  15967  2503lem2  15968  2503lem3  15969  2503prm  15970  4001lem1  15971  4001lem2  15972  4001lem3  15973  4001lem4  15974  4001prm  15975  pcoass  22945  efif1olem2  24409  mcubic  24694  quart1lem  24702  quart1  24703  quartlem1  24704  tanatan  24766  log2ublem3  24795  log2ub  24796  cht3  25019  bclbnd  25125  bpos1lem  25127  bposlem4  25132  bposlem5  25133  bposlem8  25136  2lgslem3a  25241  2lgsoddprmlem3c  25257  2lgsoddprmlem3d  25258  ex-fac  27540  ex-prmo  27548  ipasslem10  27924  siii  27938  normlem3  28199  bcsiALT  28266  dpmul1000  29837  hgt750lem2  30960  inductionexd  38872  fouriersw  40868  1t10e1p1e11  41746  1t10e1p1e11OLD  41747  fmtno5lem1  41892  fmtno5lem2  41893  257prm  41900  fmtno4prmfac  41911  fmtno4nprmfac193  41913  fmtno5faclem2  41919  139prmALT  41938  127prm  41942  2exp11  41944  mod42tp1mod8  41946  3exp4mod41  41960  41prothprmlem2  41962
  Copyright terms: Public domain W3C validator