Metamath Proof Explorer

Theorem colineartriv2

Description: Trivial case of colinearity. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colineartriv2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear B B

Proof

Step Hyp Ref Expression
1 btwntriv1 ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Btwn B A
2 1 3mix2d ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → A Btwn B B ∨ B Btwn B A ∨ B Btwn A B
3 2 3com23 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Btwn B B ∨ B Btwn B A ∨ B Btwn A B
4 simp1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → N ∈ ℕ
5 simp2 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A ∈ 𝔼 ⁡ N
6 simp3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → B ∈ 𝔼 ⁡ N
7 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear B B ↔ A Btwn B B ∨ B Btwn B A ∨ B Btwn A B
8 4 5 6 6 7 syl13anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear B B ↔ A Btwn B B ∨ B Btwn B A ∨ B Btwn A B
9 3 8 mpbird ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A Colinear B B