# List of theorems

List of theorems in general/Collinearity.gh:

(↔ (collinear x y z) (∨ (∨ (between x y z) (between y z x)) (between z x y)))
(→ (between x y z) (collinear x y z))
(↔ (collinear x y z) (collinear y z x))
(↔ (collinear x y z) (collinear x z y))
(↔ (collinear x y z) (collinear y x z))
(↔ (collinear x y z) (collinear z y x))
(collinear A A B)
(collinear A B B)
(collinear A B A)
(→ (∧ (collinear A B C) (≅ A B C A′ B′ C′)) (collinear A′ B′ C′))
(→ (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (collinear x0 x1 x2) (collinear y0 y1 y2)))
(∃ c′ φ)(→ (∧ (between x y z) (≡ A B A′ B′)) (∃ c′ (∧ (between x y z) (∧ (≡ A B A′ B′) φ))))
(→ (∧ (between A B C) (∧ (≡ A B A′ B′) (∧ (between A′ B′ C′) (≡ B′ C′ B C)))) (≡ B C B′ C′))
(→ (∧ (between A B C) (∧ (≡ A B A′ B′) (∧ (between A′ B′ C′) (≡ B′ C′ B C)))) (≡ A C A′ C′))
(→ (∧ (between A B C) (∧ (≡ A B A′ B′) (∧ (between A′ B′ C′) (≡ B′ C′ B C)))) (≅ A B C A′ B′ C′))
(→ (between A B C) (→ (≡ A B A′ B′) (∃ c′ (≅ A B C A′ B′ c′))))
(→ (∧ (between C A B) (∧ (≡ A B A′ B′) (∧ (between B′ A′ C′) (≡ A′ C′ A C)))) (≡ A C A′ C′))
(→ (∧ (between C A B) (∧ (≡ A B A′ B′) (∧ (between B′ A′ C′) (≡ A′ C′ A C)))) (≡ B C B′ C′))
(→ (∧ (between C A B) (∧ (≡ A B A′ B′) (∧ (between B′ A′ C′) (≡ A′ C′ A C)))) (≅ A B C A′ B′ C′))
(→ (between C A B) (→ (≡ A B A′ B′) (∃ c′ (≅ A B C A′ B′ c′))))
(→ (between B C A) (→ (≡ A B A′ B′) (∃ c′ (≅ A B C A′ B′ c′))))
(→ (∧ (collinear A B C) (≡ A B A′ B′)) (∃ c′ (≅ A B C A′ B′ c′)))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (¬ (= A B)))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (≡ A B A′ B′))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (≡ B C B′ C′))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (≡ A D A′ D′))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (≡ B D B′ D′))
(→ (∧ (between A B C) (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (between A′ B′ C′))
(→ (between A B C) (→ (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′)))
(→ (∧ (between B C A) (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (between B′ C′ A′))
(→ (∧ p (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (≡ C A C′ A′))
(→ (between B C A) (→ (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′)))
(→ (∧ (between B A C) (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′))) (between B′ A′ C′))
(→ (between B A C) (→ (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′)))
(→ (between C A B) (→ (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′)))
(→ (collinear A B C) (→ (∧ (∧ (∧ (¬ (= A B)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′)))
(→ (∧ (∧ (∧ (∧ p q) r) s) t) (∧ q (∧ (∧ (∧ p r) s) t)))
(→ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′))
(→ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≡ A P A Q)) (≡ B P B Q)) (≡ C P C Q))
(→ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≡ A C A C′)) (≡ B C B C′)) (= C C′))
(→ (= A B) (→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= A C)))
(→ (= A B) (→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= A C′)))
(→ (= A B) (→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= C C′)))
(→ (¬ (= A B)) (→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= C C′)))
(→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= C C′))