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

Theorem mulcomli 9601
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 9600 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2450 1  |-  ( B  x.  A )  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1872  (class class class)co 6249   CCcc 9488    x. cmul 9495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2408  ax-mulcom 9554
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421
This theorem is referenced by:  divcan1i  10302  mvllmuli  10391  recgt0ii  10463  nummul2c  11039  halfthird  11108  5recm6rec  11109  cos2bnd  14185  prmo3  14942  dec5nprm  14981  decexp2  14990  karatsuba  14999  2exp6  15001  2exp8  15003  2exp16  15004  7prm  15025  13prm  15030  17prm  15031  19prm  15032  23prm  15033  43prm  15036  83prm  15037  139prm  15038  163prm  15039  317prm  15040  631prm  15041  1259lem1  15045  1259lem2  15046  1259lem3  15047  1259lem4  15048  1259lem5  15049  1259prm  15050  2503lem1  15051  2503lem2  15052  2503lem3  15053  2503prm  15054  4001lem1  15055  4001lem2  15056  4001lem3  15057  4001lem4  15058  4001prm  15059  pcoass  21997  efif1olem2  23434  mcubic  23715  quart1lem  23723  quart1  23724  quartlem1  23725  tanatan  23787  log2ublem3  23816  log2ub  23817  cht3  24042  bclbnd  24150  bpos1lem  24152  bposlem4  24157  bposlem5  24158  bposlem8  24161  ipasslem10  26422  siii  26436  normlem3  26707  bcsiALT  26774  inductionexd  36506  fouriersw  37978  1t10e1p1e11  38523  3exp4mod41  38729  41prothprmlem2  38731
  Copyright terms: Public domain W3C validator