Metamath Proof Explorer

Theorem mul12

Description: Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005)

Ref Expression
Assertion mul12 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
2 1 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) x. C ) = ( ( B x. A ) x. C ) )
3 2 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( B x. A ) x. C ) )
4 mulass 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
5 mulass 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> ( ( B x. A ) x. C ) = ( B x. ( A x. C ) ) )
6 5 3com12 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B x. A ) x. C ) = ( B x. ( A x. C ) ) )
7 3 4 6 3eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )