merlem2 Show Code edit
# Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem2 () () (-> (-> (-> ph ph) ch) (-> th ch)) (-> ch ch) ph (-. th) ph merlem1 ch ch ph th (-> ph ph) meredith ax-mp)
(-> (-> (-> ph ph) ch) (-> th ch))
edit