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