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

Theorem mulcomli 9926
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 9925 . 2 (𝐵 · 𝐴) = (𝐴 · 𝐵)
4 mulcomli.3 . 2 (𝐴 · 𝐵) = 𝐶
53, 4eqtri 2632 1 (𝐵 · 𝐴) = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wcel 1977  (class class class)co 6549  cc 9813   · cmul 9820
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590  ax-mulcom 9879
This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603
This theorem is referenced by:  divcan1i  10648  mvllmuli  10737  recgt0ii  10808  nummul2c  11439  halfthird  11561  5recm6rec  11562  sq4e2t8  12824  cos2bnd  14757  prmo3  15583  dec5nprm  15608  decexp2  15617  karatsuba  15630  karatsubaOLD  15631  2exp6  15633  2exp8  15634  2exp16  15635  7prm  15655  13prm  15661  17prm  15662  19prm  15663  23prm  15664  43prm  15667  83prm  15668  139prm  15669  163prm  15670  317prm  15671  631prm  15672  1259lem1  15676  1259lem2  15677  1259lem3  15678  1259lem4  15679  1259lem5  15680  1259prm  15681  2503lem1  15682  2503lem2  15683  2503lem3  15684  2503prm  15685  4001lem1  15686  4001lem2  15687  4001lem3  15688  4001lem4  15689  4001prm  15690  pcoass  22632  efif1olem2  24093  mcubic  24374  quart1lem  24382  quart1  24383  quartlem1  24384  tanatan  24446  log2ublem3  24475  log2ub  24476  cht3  24699  bclbnd  24805  bpos1lem  24807  bposlem4  24812  bposlem5  24813  bposlem8  24816  2lgslem3a  24921  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  ex-fac  26700  ex-prmo  26708  ipasslem10  27078  siii  27092  normlem3  27353  bcsiALT  27420  inductionexd  37473  fouriersw  39124  1t10e1p1e11  39937  1t10e1p1e11OLD  39938  fmtno5lem1  40003  fmtno5lem2  40004  257prm  40011  fmtno4prmfac  40022  fmtno4nprmfac193  40024  fmtno5faclem2  40030  139prmALT  40049  127prm  40053  2exp11  40055  mod42tp1mod8  40057  3exp4mod41  40071  41prothprmlem2  40073
  Copyright terms: Public domain W3C validator