Metamath Proof Explorer

Theorem colinearperm3

Description: Permutation law for colinearity. Part of theorem 4.11 of Schwabhauser p. 36. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colinearperm3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ B Colinear C A

Proof

Step Hyp Ref Expression
1 3orrot ⊢ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ B Btwn C A ∨ C Btwn A B ∨ A Btwn B C
2 1 a1i ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Btwn B C ∨ B Btwn C A ∨ C Btwn A B ↔ B Btwn C A ∨ C Btwn A B ∨ A Btwn B C
3 brcolinear ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ A Btwn B C ∨ B Btwn C A ∨ C Btwn A B
4 3anrot ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N
5 brcolinear ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Colinear C A ↔ B Btwn C A ∨ C Btwn A B ∨ A Btwn B C
6 4 5 sylan2b ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Colinear C A ↔ B Btwn C A ∨ C Btwn A B ∨ A Btwn B C
7 2 3 6 3bitr4d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ B Colinear C A