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

Theorem mulcomli 10303
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 10302 . 2 (𝐵 · 𝐴) = (𝐴 · 𝐵)
4 mulcomli.3 . 2 (𝐴 · 𝐵) = 𝐶
53, 4eqtri 2787 1 (𝐵 · 𝐴) = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1652  wcel 2155  (class class class)co 6842  cc 10187   · cmul 10194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2743  ax-mulcom 10253
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758
This theorem is referenced by:  divcan1i  11023  mvllmuli  11112  recgt0ii  11183  nummul2c  11791  halfthird  11884  5recm6rec  11885  sq4e2t8  13169  cos2bnd  15202  prmo3  16026  dec5nprm  16051  decexp2  16060  karatsuba  16069  2exp6  16071  2exp8  16072  2exp16  16073  7prm  16093  13prm  16098  17prm  16099  19prm  16100  23prm  16101  43prm  16104  83prm  16105  139prm  16106  163prm  16107  317prm  16108  631prm  16109  1259lem1  16113  1259lem2  16114  1259lem3  16115  1259lem4  16116  1259lem5  16117  1259prm  16118  2503lem1  16119  2503lem2  16120  2503lem3  16121  2503prm  16122  4001lem1  16123  4001lem2  16124  4001lem3  16125  4001lem4  16126  4001prm  16127  pcoass  23102  efif1olem2  24581  mcubic  24865  quart1lem  24873  quart1  24874  quartlem1  24875  tanatan  24937  log2ublem3  24966  log2ub  24967  cht3  25190  bclbnd  25296  bpos1lem  25298  bposlem4  25303  bposlem5  25304  bposlem8  25307  2lgslem3a  25412  2lgsoddprmlem3c  25428  2lgsoddprmlem3d  25429  ex-exp  27701  ex-fac  27702  ex-prmo  27710  ipasslem10  28085  siii  28099  normlem3  28360  bcsiALT  28427  dpmul1000  29989  hgt750lem2  31113  inductionexd  39059  fouriersw  41017  1t10e1p1e11  41986  fmtno5lem1  42073  fmtno5lem2  42074  257prm  42081  fmtno4prmfac  42092  fmtno4nprmfac193  42094  fmtno5faclem2  42100  139prmALT  42119  127prm  42123  2exp11  42125  mod42tp1mod8  42127  3exp4mod41  42141  41prothprmlem2  42143
  Copyright terms: Public domain W3C validator