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

Theorem mulcomli 9649
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
mulcomli.3  |-  ( A  x.  B )  =  C
Assertion
Ref Expression
mulcomli  |-  ( B  x.  A )  =  C

Proof of Theorem mulcomli
StepHypRef Expression
1 axi.2 . . 3  |-  B  e.  CC
2 axi.1 . . 3  |-  A  e.  CC
31, 2mulcomi 9648 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2458 1  |-  ( B  x.  A )  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1870  (class class class)co 6305   CCcc 9536    x. cmul 9543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407  ax-mulcom 9602
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421
This theorem is referenced by:  divcan1i  10350  mvllmuli  10439  recgt0ii  10512  nummul2c  11088  halfthird  11157  5recm6rec  11158  cos2bnd  14220  prmo3  14962  dec5nprm  15001  decexp2  15010  karatsuba  15019  2exp6  15021  2exp8  15023  2exp16  15024  7prm  15045  13prm  15050  17prm  15051  19prm  15052  23prm  15053  43prm  15056  83prm  15057  139prm  15058  163prm  15059  317prm  15060  631prm  15061  1259lem1  15065  1259lem2  15066  1259lem3  15067  1259lem4  15068  1259lem5  15069  1259prm  15070  2503lem1  15071  2503lem2  15072  2503lem3  15073  2503prm  15074  4001lem1  15075  4001lem2  15076  4001lem3  15077  4001lem4  15078  4001prm  15079  pcoass  21948  efif1olem2  23357  mcubic  23638  quart1lem  23646  quart1  23647  quartlem1  23648  tanatan  23710  log2ublem3  23739  log2ub  23740  cht3  23963  bclbnd  24071  bpos1lem  24073  bposlem4  24078  bposlem5  24079  bposlem8  24082  ipasslem10  26325  siii  26339  normlem3  26600  bcsiALT  26667  inductionexd  36229  fouriersw  37662  1t10e1p1e11  38099  3exp4mod41  38305  41prothprmlem2  38307
  Copyright terms: Public domain W3C validator