Metamath Proof Explorer

Theorem colinearperm5

Description: Permutation law for colinearity. Part of theorem 4.11 of Schwabhauser p. 36. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearperm5 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> C Colinear <. B , A >. ) )

Proof

Step Hyp Ref Expression
1 colinearperm4 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> C Colinear <. A , B >. ) )
2 3anrot 
 |-  ( ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
3 colinearperm1 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( C Colinear <. A , B >. <-> C Colinear <. B , A >. ) )
4 2 3 sylan2br 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Colinear <. A , B >. <-> C Colinear <. B , A >. ) )
5 1 4 bitrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> C Colinear <. B , A >. ) )