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

Theorem mulcomli 10638
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 10637 . 2 (𝐵 · 𝐴) = (𝐴 · 𝐵)
4 mulcomli.3 . 2 (𝐴 · 𝐵) = 𝐶
53, 4eqtri 2841 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-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790  ax-mulcom 10589
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  divcan1i  11372  mvllmuli  11461  recgt0ii  11534  nummul2c  12136  halfthird  12229  5recm6rec  12230  sq4e2t8  13550  cos2bnd  15529  prmo3  16365  dec5nprm  16390  decexp2  16399  karatsuba  16408  2exp6  16410  2exp8  16411  2exp16  16412  7prm  16432  13prm  16437  17prm  16438  19prm  16439  23prm  16440  43prm  16443  83prm  16444  139prm  16445  163prm  16446  317prm  16447  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  1259prm  16457  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  pcoass  23555  efif1olem2  25054  mcubic  25352  quart1lem  25360  quart1  25361  quartlem1  25362  tanatan  25424  log2ublem3  25453  log2ub  25454  cht3  25677  bclbnd  25783  bpos1lem  25785  bposlem4  25790  bposlem5  25791  bposlem8  25794  2lgslem3a  25899  2lgsoddprmlem3c  25915  2lgsoddprmlem3d  25916  ex-exp  28156  ex-fac  28157  ex-prmo  28165  ipasslem10  28543  siii  28557  normlem3  28816  bcsiALT  28883  dpmul1000  30502  hgt750lem2  31822  235t711  39055  ex-decpmul  39056  3cubeslem3l  39161  3cubeslem3r  39162  inductionexd  40383  fouriersw  42393  1t10e1p1e11  43387  fmtno5lem1  43592  fmtno5lem2  43593  257prm  43600  fmtno4prmfac  43611  fmtno4nprmfac193  43613  fmtno5faclem2  43619  139prmALT  43636  127prm  43640  2exp11  43642  mod42tp1mod8  43644  3exp4mod41  43658  41prothprmlem2  43660  2exp340mod341  43775  8exp8mod9  43778
  Copyright terms: Public domain W3C validator