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 imbitrrid ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → C Btwn A B → A Colinear B C