List of theorems

List of theorems in general/From_intuitionistic_to_classical_propositional_logic.gh:

(→ (¬ (¬ p)) p)
(¬ (¬ p))p
(↔ p (¬ (¬ p)))
(→ (→ (¬ q) (¬ p)) (→ p q))
(→ (¬ q) (¬ p))(→ p q)
(↔ (→ p q) (→ (¬ q) (¬ p)))
(↔ (→ (¬ p) q) (→ (¬ q) p))
(→ (¬ p) q)(→ (¬ q) p)
(↔ (→ p (¬ q)) (→ q (¬ p)))
(→ p (¬ q))(→ q (¬ p))
(↔ (↔ p q) (↔ (¬ p) (¬ q)))
(↔ (¬ p) (¬ q))(↔ p q)
(↔ (↔ p (¬ q)) (↔ q (¬ p)))
(↔ p (¬ q))(↔ q (¬ p))
(↔ (↔ (¬ p) q) (↔ (¬ q) p))
(↔ (¬ p) q)(↔ (¬ q) p)
(↔ (¬ (∨ p q)) (∧ (¬ p) (¬ q)))
(↔ (¬ (∨ p (¬ q))) (∧ (¬ p) q))
(↔ (¬ (∨ (¬ p) q)) (∧ p (¬ q)))
(↔ (¬ (∨ (¬ p) (¬ q))) (∧ p q))
(↔ (¬ (∧ p q)) (∨ (¬ p) (¬ q)))
(↔ (¬ (∧ p (¬ q))) (∨ (¬ p) q))
(↔ (¬ (∧ (¬ p) q)) (∨ p (¬ q)))
(↔ (¬ (∧ (¬ p) (¬ q))) (∨ p q))
(¬ (∨ p (¬ q)))(∧ (¬ p) q)
(¬ (∨ (¬ p) q))(∧ p (¬ q))
(¬ (∨ (¬ p) (¬ q)))(∧ p q)
(¬ (∧ p q))(∨ (¬ p) (¬ q))
(¬ (∧ p (¬ q)))(∨ (¬ p) q)
(¬ (∧ (¬ p) q))(∨ p (¬ q))
(¬ (∧ (¬ p) (¬ q)))(∨ p q)
(∨ p (¬ q))(¬ (∧ (¬ p) q))
(∨ (¬ p) q)(¬ (∧ p (¬ q)))
(∧ p (¬ q))(¬ (∨ (¬ p) q))
(∧ (¬ p) q)(¬ (∨ p (¬ q)))
(↔ (∨ p (¬ p)) (⊤))
(↔ (∨ p q) (→ (¬ p) q))
(↔ (→ p q) (∨ (¬ p) q))
(→ p q)(∨ (¬ p) q)
(→ (¬ p) q)(∨ p q)
(↔ (↔ p q) (∧ (∨ (¬ p) q) (∨ p (¬ q))))
(→ (↔ p q) (∨ p (¬ q)))
(→ (↔ p q) (∨ (¬ p) q))
(↔ p q)(∧ (∨ (¬ p) q) (∨ p (¬ q)))
(↔ p q)(∨ p (¬ q))
(↔ p q)(∨ (¬ p) q)
(↔ (∨ (¬ p) q) (∧ (∨ p (¬ p)) (∨ q (¬ p))))
(↔ (∨ p (¬ q)) (∧ (∨ p (¬ q)) (∨ q (¬ q))))
(↔ (↔ p q) (∨ (∧ p q) (∧ (¬ p) (¬ q))))
(↔ p q)(∨ (∧ p q) (∧ (¬ p) (¬ q)))
(∨ (∧ p q) (∧ (¬ p) (¬ q)))(↔ p q)
(→ (∧ (→ p q) (→ (¬ p) q)) q)
(→ p q) , (→ (¬ p) q)q