Metamath Proof Explorer

Theorem colinearperm5

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

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

Proof

Step Hyp Ref Expression
1 colinearperm4 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔CColinearAB
2 3anrot ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
3 colinearperm1 ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→CColinearAB↔CColinearBA
4 2 3 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CColinearAB↔CColinearBA
5 1 4 bitrd ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔CColinearBA