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∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB→CColinearAB

Proof

Step Hyp Ref Expression
1 btwncolinear1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB→AColinearBC
2 colinearperm4 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔CColinearAB
3 1 2 sylibd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB→CColinearAB