merlem6 Show Code edit
# Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem6 () () (-> ch (-> (-> (-> ps ch) ph) (-> th ph))) (-> ps ch) ph th merlem4 ps ch (-> (-> (-> ps ch) ph) (-> th ph)) merlem3 ax-mp)
(-> ch (-> (-> (-> ps ch) ph) (-> th ph)))
edit