Metamath Proof Explorer

Theorem colinearperm4

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

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

Proof

Step Hyp Ref Expression
1 colinearperm3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ B Colinear C A
2 3anrot ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ↔ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N
3 colinearperm3 ⊢ N ∈ ℕ ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ A ∈ 𝔼 ⁡ N → B Colinear C A ↔ C Colinear A B
4 2 3 sylan2b ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → B Colinear C A ↔ C Colinear A B
5 1 4 bitrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A Colinear B C ↔ C Colinear A B