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