Metamath Proof Explorer

Theorem colinearperm4

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

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

Proof

Step Hyp Ref Expression
1 colinearperm3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> B Colinear <. C , A >. ) )
2 3anrot 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
3 colinearperm3 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( B Colinear <. C , A >. <-> C Colinear <. A , B >. ) )
4 2 3 sylan2b 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Colinear <. C , A >. <-> C Colinear <. A , B >. ) )
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 <. A , B >. ) )