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

Theorem mulcomli 10639
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 10638 . 2 (𝐵 · 𝐴) = (𝐴 · 𝐵)
4 mulcomli.3 . 2 (𝐴 · 𝐵) = 𝐶
53, 4eqtri 2845 1 (𝐵 · 𝐴) = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2114  (class class class)co 7140  cc 10524   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794  ax-mulcom 10590
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  divcan1i  11373  mvllmuli  11462  recgt0ii  11535  nummul2c  12136  halfthird  12229  5recm6rec  12230  sq4e2t8  13558  cos2bnd  15532  prmo3  16366  dec5nprm  16391  decexp2  16400  karatsuba  16409  2exp6  16412  2exp8  16414  2exp16  16415  7prm  16435  13prm  16440  17prm  16441  19prm  16442  23prm  16443  43prm  16446  83prm  16447  139prm  16448  163prm  16449  317prm  16450  631prm  16451  1259lem1  16455  1259lem2  16456  1259lem3  16457  1259lem4  16458  1259lem5  16459  1259prm  16460  2503lem1  16461  2503lem2  16462  2503lem3  16463  2503prm  16464  4001lem1  16465  4001lem2  16466  4001lem3  16467  4001lem4  16468  4001prm  16469  pcoass  23627  efif1olem2  25133  mcubic  25431  quart1lem  25439  quart1  25440  quartlem1  25441  tanatan  25503  log2ublem3  25532  log2ub  25533  cht3  25756  bclbnd  25862  bpos1lem  25864  bposlem4  25869  bposlem5  25870  bposlem8  25873  2lgslem3a  25978  2lgsoddprmlem3c  25994  2lgsoddprmlem3d  25995  ex-exp  28233  ex-fac  28234  ex-prmo  28242  ipasslem10  28620  siii  28634  normlem3  28893  bcsiALT  28960  dpmul1000  30585  hgt750lem2  31997  12lcm5e60  39257  60lcm7e420  39259  420lcm8e840  39260  3lexlogpow5ineq1  39302  235t711  39429  ex-decpmul  39430  3cubeslem3l  39557  3cubeslem3r  39558  sqrtcval2  40272  resqrtvalex  40275  inductionexd  40791  fouriersw  42812  1t10e1p1e11  43806  fmtno5lem1  44009  fmtno5lem2  44010  257prm  44017  fmtno4prmfac  44028  fmtno4nprmfac193  44030  fmtno5faclem2  44036  139prmALT  44052  127prm  44055  2exp11  44057  mod42tp1mod8  44059  3exp4mod41  44073  41prothprmlem2  44075  2exp340mod341  44190  8exp8mod9  44193
  Copyright terms: Public domain W3C validator