List of theorems

List of theorems in general/from_propositional_to_prop.gh:

(↔ (-. p) (¬ p))
(↔ (-> p q) (→ p q))
symbolizeImplication Convert -> to →
(-> p q)(→ p q)
desymbolizeImplication Convert → to ->
(→ p q)(-> p q)
p , (-> p q)q
(-> p (-> q p))
ax-2 AntecedentDistribution is just a biconditionalized version of ax-2. We just need to get rid of one direction and convert the symbols.
(-> (-> p (-> q r)) (-> (-> p q) (-> p r)))
(-> (-> (-. q) (-. p)) (-> p q))