Metamath Proof Explorer

Theorem colinearperm1

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

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

Proof

Step Hyp Ref Expression
1 btwncom ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔ABtwnCB
2 3anrot ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N
3 btwncom ⊢N∈ℕ∧B∈𝔼⁡N∧C∈𝔼⁡N∧A∈𝔼⁡N→BBtwnCA↔BBtwnAC
4 2 3 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→BBtwnCA↔BBtwnAC
5 3anrot ⊢C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N↔A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N
6 btwncom ⊢N∈ℕ∧C∈𝔼⁡N∧A∈𝔼⁡N∧B∈𝔼⁡N→CBtwnAB↔CBtwnBA
7 5 6 sylan2br ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→CBtwnAB↔CBtwnBA
8 1 4 7 3orbi123d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB↔ABtwnCB∨BBtwnAC∨CBtwnBA
9 3orcomb ⊢ABtwnCB∨BBtwnAC∨CBtwnBA↔ABtwnCB∨CBtwnBA∨BBtwnAC
10 8 9 bitrdi ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC∨BBtwnCA∨CBtwnAB↔ABtwnCB∨CBtwnBA∨BBtwnAC
11 brcolinear ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔ABtwnBC∨BBtwnCA∨CBtwnAB
12 3ancomb ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N↔A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N
13 brcolinear ⊢N∈ℕ∧A∈𝔼⁡N∧C∈𝔼⁡N∧B∈𝔼⁡N→AColinearCB↔ABtwnCB∨CBtwnBA∨BBtwnAC
14 12 13 sylan2b ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearCB↔ABtwnCB∨CBtwnBA∨BBtwnAC
15 10 11 14 3bitr4d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→AColinearBC↔AColinearCB