Metamath Proof Explorer

Theorem outsideofcol

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

Ref Expression
Assertion outsideofcol 
|- ( P OutsideOf <. Q , R >. -> P Colinear <. Q , R >. )

Proof

Step Hyp Ref Expression
1 broutsideof 
 |-  ( P OutsideOf <. Q , R >. <-> ( P Colinear <. Q , R >. /\ -. P Btwn <. Q , R >. ) )
2 1 simplbi 
 |-  ( P OutsideOf <. Q , R >. -> P Colinear <. Q , R >. )