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

Theorem mul12i 10826
 Description: Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Hypotheses
Ref Expression
mul.1 𝐴 ∈ ℂ
mul.2 𝐵 ∈ ℂ
mul.3 𝐶 ∈ ℂ
Assertion
Ref Expression
mul12i (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))

Proof of Theorem mul12i
StepHypRef Expression
1 mul.1 . 2 𝐴 ∈ ℂ
2 mul.2 . 2 𝐵 ∈ ℂ
3 mul.3 . 2 𝐶 ∈ ℂ
4 mul12 10796 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶)))
51, 2, 3, 4mp3an 1458 1 (𝐴 · (𝐵 · 𝐶)) = (𝐵 · (𝐴 · 𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10526   · cmul 10533 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-8 2113  ax-9 2121  ax-ext 2770  ax-mulcom 10592  ax-mulass 10594 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138 This theorem is referenced by:  decmul10add  12157  faclbnd4lem1  13651  bpoly3  15406  decsplit  16411  root1eq1  25351  cxpeq  25353  1cubrlem  25434  efiatan2  25510  2efiatan  25511  tanatan  25512  log2ublem2  25540  log2ublem3  25541  bposlem8  25882  ax5seglem7  26736  ip1ilem  28616  ipasslem10  28629  polid2i  28947  3exp4mod41  44149
 Copyright terms: Public domain W3C validator