Metamath Proof Explorer

Theorem colinearperm2

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

Ref Expression
Assertion colinearperm2 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔BColinearAC

Proof

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