Metamath Proof Explorer


Theorem mul13d

Description: Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mul13d.1
|- ( ph -> A e. CC )
mul13d.2
|- ( ph -> B e. CC )
mul13d.3
|- ( ph -> C e. CC )
Assertion mul13d
|- ( ph -> ( A x. ( B x. C ) ) = ( C x. ( B x. A ) ) )

Proof

Step Hyp Ref Expression
1 mul13d.1
 |-  ( ph -> A e. CC )
2 mul13d.2
 |-  ( ph -> B e. CC )
3 mul13d.3
 |-  ( ph -> C e. CC )
4 1 2 3 mul12d
 |-  ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
5 2 1 3 mulassd
 |-  ( ph -> ( ( B x. A ) x. C ) = ( B x. ( A x. C ) ) )
6 2 1 mulcld
 |-  ( ph -> ( B x. A ) e. CC )
7 6 3 mulcomd
 |-  ( ph -> ( ( B x. A ) x. C ) = ( C x. ( B x. A ) ) )
8 4 5 7 3eqtr2d
 |-  ( ph -> ( A x. ( B x. C ) ) = ( C x. ( B x. A ) ) )