Metamath Proof Explorer


Theorem mul12i

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)

Ref Expression
Hypotheses mul.1 โŠข ๐ด โˆˆ โ„‚
mul.2 โŠข ๐ต โˆˆ โ„‚
mul.3 โŠข ๐ถ โˆˆ โ„‚
Assertion mul12i ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) )

Proof

Step Hyp Ref Expression
1 mul.1 โŠข ๐ด โˆˆ โ„‚
2 mul.2 โŠข ๐ต โˆˆ โ„‚
3 mul.3 โŠข ๐ถ โˆˆ โ„‚
4 mul12 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) ) )
5 1 2 3 4 mp3an โŠข ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) )