This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mul31

Description: Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013)

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

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
2 1 oveq2d 
 |-  ( ( B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( A x. ( C x. B ) ) )
3 2 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( A x. ( C x. B ) ) )
4 mulass 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
5 mulcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C x. B ) e. CC )
6 5 ancoms 
 |-  ( ( B e. CC /\ C e. CC ) -> ( C x. B ) e. CC )
7 6 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C x. B ) e. CC )
8 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
9 7 8 mulcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C x. B ) x. A ) = ( A x. ( C x. B ) ) )
10 3 4 9 3eqtr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )