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

Theorem mul32i 11410
Description: Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.)
Hypotheses
Ref Expression
mul.1 ๐ด โˆˆ โ„‚
mul.2 ๐ต โˆˆ โ„‚
mul.3 ๐ถ โˆˆ โ„‚
Assertion
Ref Expression
mul32i ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ต)

Proof of Theorem mul32i
StepHypRef Expression
1 mul.1 . 2 ๐ด โˆˆ โ„‚
2 mul.2 . 2 ๐ต โˆˆ โ„‚
3 mul.3 . 2 ๐ถ โˆˆ โ„‚
4 mul32 11380 . 2 ((๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚) โ†’ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ต))
51, 2, 3, 4mp3an 1462 1 ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ต)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   โˆˆ wcel 2107  (class class class)co 7409  โ„‚cc 11108   ยท cmul 11115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-mulcom 11174  ax-mulass 11176
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412
This theorem is referenced by:  8th4div3  12432  faclbnd4lem1  14253  bpoly4  16003  dec5nprm  16999  dec2nprm  17000  karatsuba  17017  quart1lem  26360  log2ublem2  26452  log2ub  26454  normlem3  30396  bcseqi  30404  dpmul100  32094  dpmul1000  32096
  Copyright terms: Public domain W3C validator