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→AColinearBC↔BColinearCA

Proof

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