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