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

Theorem mul12 9534
Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
Assertion
Ref Expression
mul12  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )

Proof of Theorem mul12
StepHypRef Expression
1 mulcom 9367 . . . 4  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
21oveq1d 6105 . . 3  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  x.  B )  x.  C
)  =  ( ( B  x.  A )  x.  C ) )
323adant3 1008 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( ( B  x.  A )  x.  C ) )
4 mulass 9369 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
5 mulass 9369 . . 3  |-  ( ( B  e.  CC  /\  A  e.  CC  /\  C  e.  CC )  ->  (
( B  x.  A
)  x.  C )  =  ( B  x.  ( A  x.  C
) ) )
653com12 1191 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( B  x.  A
)  x.  C )  =  ( B  x.  ( A  x.  C
) ) )
73, 4, 63eqtr3d 2482 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  x.  C ) )  =  ( B  x.  ( A  x.  C )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756  (class class class)co 6090   CCcc 9279    x. cmul 9286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-mulcom 9345  ax-mulass 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-iota 5380  df-fv 5425  df-ov 6093
This theorem is referenced by:  mul02  9546  mul12i  9563  mul12d  9577  mulre  12609  sqreulem  12846  demoivre  13483  demoivreALT  13484  dvdscmul  13558  dvdscmulr  13560  dvdstr  13565  ablfacrp  16566  nmoleub2lem3  20669  sinperlem  21941  coskpi  21981  sineq0  21982  efif1olem4  22000  rpvmasum2  22760  fsumcube  28202  expgrowthi  29605
  Copyright terms: Public domain W3C validator