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 ) ) ) |
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 ) ) ) |