Metamath Proof Explorer


Theorem btwncolinear1

Description: Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion btwncolinear1 N A 𝔼 N B 𝔼 N C 𝔼 N C Btwn A B A Colinear B C

Proof

Step Hyp Ref Expression
1 3mix3 C Btwn A B A Btwn B C B Btwn C A C Btwn A B
2 brcolinear N A 𝔼 N B 𝔼 N C 𝔼 N A Colinear B C A Btwn B C B Btwn C A C Btwn A B
3 1 2 syl5ibr N A 𝔼 N B 𝔼 N C 𝔼 N C Btwn A B A Colinear B C