# List of theorems

List of theorems in general/Convenience_theorems_of_propositional_logic.gh:

p , (→ (∧ p q) r)(→ q r)
q , (→ (∧ p q) r)(→ p r)
p , (→ (∧ (∧ p q) r) consequent)(→ (∧ q r) consequent)
q , (→ (∧ (∧ p q) r) consequent)(→ (∧ p r) consequent)
p , (→ (∧ (∧ (∧ p q) r) s) consequent)(→ (∧ (∧ q r) s) consequent)
(→ p (→ q r))(→ q (→ p r))
p , (→ antecedent (→ p q))(→ antecedent q)
q , (→ p (↔ q r))(→ p r)
r , (→ p (↔ q r))(→ p q)
(¬ r) , (→ p (↔ q r))(→ p (¬ q))
(¬ q) , (→ p (↔ q r))(→ p (¬ r))
(¬ r) , (→ p (→ q r))(→ p (¬ q))
(→ p q) , (↔ p r)(→ r q)
(→ antecedent (→ p q)) , (↔ q r)(→ antecedent (→ p r))
(→ antecedent (→ p q)) , (↔ p r)(→ antecedent (→ r q))
(→ antecedent (↔ p q)) , (↔ p r)(→ antecedent (↔ r q))
(→ antecedent (↔ p q)) , (↔ q r)(→ antecedent (↔ p r))
(∨ p q) , (↔ q r)(∨ p r)
(↔ (∧ p q) (¬ (→ p (¬ q))))
(↔ (→ p q) (¬ (∧ p (¬ q))))
(→ (⊥) p)
(→ (→ p (⊥)) (∧ (→ p (⊥)) (→ (⊥) p)))
(↔ (→ p (⊥)) (↔ p (⊥)))
(↔ (¬ p) (↔ p (⊥)))
(→ (↔ p q) (↔ (∨ r p) (∨ r q)))
(↔ p q)(↔ (∨ r p) (∨ r q))
(→ (↔ p q) (↔ (∨ p common) (∨ q common)))
(↔ p q)(↔ (∨ p common) (∨ q common))
(↔ p q)(↔ (∧ r p) (∧ r q))
(↔ p q)(↔ (∧ p r) (∧ q r))
(→ (↔ p q) (↔ (↔ p common) (↔ q common)))
(↔ p q)(↔ (↔ common p) (↔ common q))
(→ (↔ p q) (↔ (→ p common) (→ q common)))
(→ (↔ p q) (↔ (→ p common) (→ q common)))
(↔ p q)(↔ (→ p common) (→ q common))
(↔ p q)(↔ (→ common p) (→ common q))
(→ antecedent (↔ p q))(→ antecedent (↔ (¬ p) (¬ q)))
(→ antecedent (↔ p q))(→ antecedent (↔ (∧ p common) (∧ q common)))
(→ antecedent (↔ p q))(→ antecedent (↔ (∧ common p) (∧ common q)))
(→ antecedent (↔ p q))(→ antecedent (↔ (∨ p common) (∨ q common)))
(→ antecedent (↔ p q))(→ antecedent (↔ (∨ common p) (∨ common q)))
(→ antecedent (↔ p0 q0)) , (→ antecedent (↔ p1 q1))(→ antecedent (↔ (∧ p0 p1) (∧ q0 q1)))
(→ antecedent (↔ p0 q0)) , (→ antecedent (↔ p1 q1))(→ antecedent (↔ (∨ p0 p1) (∨ q0 q1)))
(→ antecedent (↔ p q))(→ antecedent (↔ (→ p common) (→ q common)))
(→ antecedent (↔ p q))(→ antecedent (↔ (→ common p) (→ common q)))
(→ antecedent (↔ p0 q0)) , (→ antecedent (↔ p1 q1))(→ antecedent (↔ (→ p0 p1) (→ q0 q1)))
(→ antecedent (↔ p0 q0)) , (→ antecedent (↔ p1 q1))(→ antecedent (↔ (↔ p0 p1) (↔ q0 q1)))
(→ antecedent (↔ p q))(→ antecedent (↔ (↔ common p) (↔ common q)))
(→ antecedent (↔ p q))(→ antecedent (↔ (↔ p common) (↔ q common)))
(→ antecedent (∨ p q)) , (↔ p r)(→ antecedent (∨ r q))
(→ antecedent (→ p q)) , (→ antecedent (→ q p))(→ antecedent (↔ p q))
(→ antecedent (↔ p q))(→ antecedent (→ p q))
(→ antecedent (↔ p q))(→ antecedent (→ q p))
(→ antecedent p) , (→ antecedent (→ p q))(→ antecedent q)
(→ antecedent (↔ p q)) , (→ antecedent (↔ q r))(→ antecedent (↔ p r))
(→ antecedent (↔ p q))(→ antecedent (↔ q p))
(→ antecedent p)(→ antecedent (→ q p))
(→ antecedent (→ p (→ q r)))(→ antecedent (→ (∧ p q) r))
(→ antecedent (→ (∧ p q) r))(→ antecedent (→ p (→ q r)))
(→ antecedent (∧ p q))(→ antecedent q)
(→ antecedent (∧ p q))(→ antecedent p)
(→ antecedent (→ p q))(→ antecedent (→ (¬ q) (¬ p)))
(→ antecedent (→ (¬ q) (¬ p)))(→ antecedent (→ p q))
(→ antecedent p) , q(→ antecedent (∧ q p))
(→ antecedent p) , q(→ antecedent (∧ p q))
(→ (→ p (→ q r)) consequent)(→ (→ (∧ p q) r) consequent)
(→ (→ (∧ p q) r) consequent)(→ (→ p (→ q r)) consequent)
(→ antecedent (∧ (∧ p q) r))(→ antecedent (∧ p (∧ q r)))
(→ antecedent (∧ p (∧ q r)))(→ antecedent (∧ (∧ p q) r))
(↔ (∨ (∨ p q) (∨ r s)) (∨ (∨ p r) (∨ q s)))
(∨ (∨ p q) (∨ r s))(∨ (∨ p r) (∨ q s))
(↔ (∨ (∨ p q) r) (∨ (∨ p r) q))
(∨ (∨ p q) r)(∨ (∨ p r) q)
(∨ (∨ p q) r)(∨ (∨ q p) r)
(↔ (∧ (∧ p q) (∧ r s)) (∧ (∧ p r) (∧ q s)))
(→ p q) , (→ p (¬ q))(¬ p)
(→ p (¬ p))(¬ p)
(→ (¬ p) p)p