Metamath Proof Explorer

Theorem btwncolinear5

Description: Betweenness implies colinearity. (Contributed by Scott Fenton, 15-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Step	Hyp	Ref	Expression
1		btwncolinear1	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )
2		colinearperm4	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> C Colinear <. A , B >. ) )
3	1 2	sylibd	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> C Colinear <. A , B >. ) )

Step

Hyp

Ref

Expression

 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )

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

1 2

 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> C Colinear <. A , B >. ) )