merlem8 Show Code edit
# Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem8 () () (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) ph ph ph ph ph meredith (-> (-> (-> (-> (-> ph ph) (-> (-. ph) (-. ph))) ph) ph) (-> (-> ph ph) (-> ph ph))) ps ch th ta merlem7 ax-mp)
(-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th))
edit