# List of theorems

List of theorems in general/First-order_logic.gh:

(→ (∀ x (→ φ ψ)) (→ (∀ x φ) (∀ x ψ)))
(→ φ ψ)(→ (∀ x φ) (∀ x ψ))
(↔ φ ψ)(↔ (∀ x φ) (∀ x ψ))
(= x x)
(↔ (= x y) (= y x))
(= s t)(= t s)
(→ (∧ (= x y) (= y z)) (= x z))
(= s t) , (= t u)(= s u)
(→ (= y x) (→ (¬ φ) (∀ x (→ (= x y) (¬ φ)))))
(→ (∀ x (→ (= x y) (¬ φ))) (∀ x (→ φ (¬ (= x y)))))
(→ (∀ x (→ φ (¬ (= x y)))) (¬ (∀ x φ)))
(→ (¬ (→ (∀ x φ) φ)) (¬ (= y x)))
(→ (∀ y (¬ (→ (∀ x φ) φ))) (∀ y (¬ (= y x))))
(→ (∀ x φ) φ)
(∀ x φ)φ
(→ (∀ x (¬ (∀ x (¬ (∀ x φ))))) (∀ x (∀ x φ)))
(→ (∀ x φ) (∀ x (∀ x φ)))
(→ (∀ x φ) ψ)(→ (∀ x φ) (∀ x ψ))
(↔ (∃ x φ) (¬ (∀ x (¬ φ))))
(↔ (¬ (∃ x φ)) (∀ x (¬ φ)))
(↔ (¬ (∀ x φ)) (∃ x (¬ φ)))
(→ φ ψ)(→ (∃ x φ) (∃ x ψ))
(↔ φ ψ)(↔ (∃ x φ) (∃ x ψ))
(→ φ (∃ x φ))
(→ (∀ x (→ φ ψ)) (→ (∃ x φ) (∃ x ψ)))
(↔ (∀ x (∀ y φ)) (∀ y (∀ x φ)))
(↔ (∃ x (∃ y φ)) (∃ y (∃ x φ)))
(→ (∀ x (∧ φ ψ)) (∧ (∀ x φ) (∀ x ψ)))
(→ (∧ (∀ x φ) (∀ x ψ)) (∀ x (∧ φ ψ)))
(↔ (∀ x (∧ φ ψ)) (∧ (∀ x φ) (∀ x ψ)))
(↔ (∃ x (∨ φ ψ)) (∨ (∃ x φ) (∃ x ψ)))
(→ (∃ x (∧ φ ψ)) (∧ (∃ x φ) (∃ x ψ)))
(→ (∀ x (↔ φ ψ)) (↔ (∀ x φ) (∀ x ψ)))
(↔ (∃ x (→ φ ψ)) (→ (∀ x φ) (∃ x ψ)))
(→ (∧ (∀ x φ) (∃ x ψ)) (∃ x (∧ φ ψ)))
(→ (∧ (∃ x φ) (∀ x ψ)) (∃ x (∧ φ ψ)))
(∃ x φ) , (∀ x ψ)(∃ x (∧ φ ψ))
(→ (¬ (∀ x (¬ (∀ x φ)))) φ)
(↔ (is-not-free-in x φ) (→ φ (∀ x φ)))
φ(is-not-free-in x φ)
(is-not-free-in x φ)
(is-not-free-in x (∀ x φ))
(is-not-free-in x φ)(is-not-free-in x (∀ y φ))
(→ (∀ x (is-not-free-in x φ)) (is-not-free-in x (¬ φ)))
(is-not-free-in x φ)(is-not-free-in x (¬ φ))
(↔ φ ψ)(↔ (is-not-free-in x φ) (is-not-free-in x ψ))
(is-not-free-in x (∃ x φ))
(is-not-free-in x φ)(is-not-free-in x (∃ y φ))
(is-not-free-in x φ) , (→ φ ψ)(→ φ (∀ x ψ))
(→ φ ψ)(→ φ (∀ x ψ))
(→ (¬ φ) (→ φ ψ))
(is-not-free-in x φ) , (is-not-free-in x ψ)(is-not-free-in x (→ φ ψ))
(is-not-free-in x φ) , (is-not-free-in x ψ)(is-not-free-in x (∨ φ ψ))
(is-not-free-in x φ) , (is-not-free-in x ψ)(is-not-free-in x (∧ φ ψ))
(is-not-free-in x φ) , (is-not-free-in x ψ)(is-not-free-in x (↔ φ ψ))
(↔ (∀ x φ) φ)
(↔ (∃ x φ) φ)
(is-not-free-in x φ)(↔ (∃ x φ) φ)
(↔ (∃ x φ) φ)
(∃ x φ)φ
(→ antecedent (∃ x φ))(→ antecedent φ)
(is-not-free-in x φ)(↔ (∀ x φ) φ)
(is-not-free-in x φ)(↔ (∀ x (→ φ ψ)) (→ φ (∀ x ψ)))
(∀ x (→ φ ψ)) , (is-not-free-in x φ)(→ φ (∀ x ψ))
(→ φ (∀ x ψ)) , (is-not-free-in x φ)(∀ x (→ φ ψ))
(is-not-free-in x φ)(↔ (∃ x (→ φ ψ)) (→ φ (∃ x ψ)))
ForAllImplicationConsequentMovementNotFree This is just here until we can convert everything over to ForAllImplicationConsequentMovement.
(is-not-free-in x ψ)(↔ (∀ x (→ φ ψ)) (→ (∃ x φ) ψ))
(↔ (∀ x (→ φ ψ)) (→ (∃ x φ) ψ))
(is-not-free-in x ψ)(↔ (∃ x (→ φ ψ)) (→ (∀ x φ) ψ))
(is-not-free-in x φ)(↔ (∀ x (∨ φ ψ)) (∨ φ (∀ x ψ)))
(is-not-free-in x φ)(↔ (∃ x (∨ φ ψ)) (∨ φ (∃ x ψ)))
(↔ (∃ x (∨ φ ψ)) (∨ φ (∃ x ψ)))
(↔ (∃ x (∨ φ ψ)) (∨ (∃ x φ) ψ))
(is-not-free-in x φ)(↔ (∀ x (∧ φ ψ)) (∧ φ (∀ x ψ)))
(is-not-free-in x φ)(↔ (∃ x (∧ φ ψ)) (∧ φ (∃ x ψ)))
(↔ (∃ x (∧ φ ψ)) (∧ φ (∃ x ψ)))
(↔ (∃ x (∧ φ ψ)) (∧ (∃ x φ) ψ))
(↔ (∃ x (→ φ ψ)) (→ φ (∃ x ψ)))
(→ antecedent (∧ φ (∃ x ψ)))(→ antecedent (∃ x (∧ φ ψ)))
(→ antecedent (∧ (∃ x φ) ψ))(→ antecedent (∃ x (∧ φ ψ)))
(→ antecedent (∃ x ψ))(→ antecedent (∃ x (∧ antecedent ψ)))
(→ φ ψ)(→ (∃ x φ) ψ)
(↔ (∃ x (∃ y (∧ φx ψy))) (∧ (∃ x φx) (∃ y ψy)))
(→ antecedent (∧ (∃ x φx) (∃ y ψy)))(→ antecedent (∃ x (∃ y (∧ φx ψy))))
(→ (∃ x (∀ y φ)) (∀ y (∃ x φ)))
(∃ x (= x y))
(→ (∀ x (→ (= x y) (∀ x φ))) φ)
(↔ (∀ x (→ φ (¬ ψ))) (¬ (∃ x (∧ φ ψ))))
(↔ (∃ x (∧ (= x s) φ)) (¬ (∀ x (→ (= x s) (¬ φ)))))
(is-not-free-in x φy) , (is-not-free-in y φx) , (→ (= x y) (↔ φx φy))(→ (∃ y φy) (∃ x φx))
(is-not-free-in x φy) , (is-not-free-in y φx) , (→ (= x y) (↔ φx φy))(→ (∃ x φx) (∃ y φy))
(is-not-free-in x φy) , (is-not-free-in y φx) , (→ (= x y) (↔ φx φy))(↔ (∃ x φx) (∃ y φy))
(→ (= x y) (↔ φx φy))(↔ (∃ x φx) (∃ y φy))
(is-not-free-in x φy) , (is-not-free-in y φx) , (→ (= x y) (↔ φx φy))(↔ (∀ x φx) (∀ y φy))
(→ (= x y) (↔ φx φy))(↔ (∀ x φx) (∀ y φy))
(→ (∀ x (↔ φ ψ)) (↔ (∃ x φ) (∃ x ψ)))
(→ φ (↔ ψ χ))(→ φ (↔ (∃ x ψ) (∃ x χ)))
(→ φ (↔ ψ χ))(→ φ (↔ (∀ x ψ) (∀ x χ)))