# List of theorems

List of theorems in general/Line_segment_congruence.gh:

(≡ x y x y)
(→ (≡ x y z w) (≡ z w x y))
(↔ (≡ x y z w) (≡ z w x y))
(→ antecedent (≡ x y z w))(→ antecedent (≡ z w x y))
(→ (∧ (≡ x y z w) (≡ z w u v)) (≡ x y u v))
(→ (≡ x y z w) (≡ y x z w))
(↔ (≡ x y z w) (≡ y x z w))
(→ antecedent (≡ x y z w))(→ antecedent (≡ y x z w))
(↔ (≡ x y z w) (≡ x y w z))
(→ antecedent (≡ x y z w))(→ antecedent (≡ x y w z))
(≡ y y x x)
(→ (≡ x x y z) (= y z))
(↔ (≡ x y z w) (≡ y x w z))
(→ antecedent (≡ x y z w))(→ antecedent (≡ y x w z))
(→ (= x y) (→ (≡ x y z w) (= z w)))
(→ (= x y) (→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x y x′ y′)) (≡ y z y′ z′)) (≡ x z x′ z′)))
(→ (¬ (= x y)) (→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x y x′ y′)) (≡ y z y′ z′)) (≡ x z x′ z′)))
(→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x y x′ y′)) (≡ y z y′ z′)) (≡ x z x′ z′))
(→ (∧ (∧ (∧ (∧ (¬ (= Q A)) (between Q A x)) (≡ A x B C)) (between Q A y)) (≡ A y B C)) (≡ A x A y))
(→ (∧ (∧ (∧ (∧ (¬ (= Q A)) (between Q A x)) (≡ A x B C)) (between Q A y)) (≡ A y B C)) (≡ Q x Q y))
(→ (∧ (∧ (∧ (∧ (¬ (= Q A)) (between Q A x)) (≡ A x B C)) (between Q A y)) (≡ A y B C)) (≡ x x x y))
(→ (∧ (∧ (∧ (∧ (¬ (= Q A)) (between Q A x)) (≡ A x B C)) (between Q A y)) (≡ A y B C)) (= x y))