merlem11 Show Code edit
# Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem11 () () (-> (-> ph (-> ph ps)) (-> ph ps)) ph ph ph ph ph meredith ph ps (-> ph (-> ph ps)) merlem10 (-> ph (-> ph ps)) (-> ph ps) (-> (-> (-> (-> (-> ph ph) (-> (-. ph) (-. ph))) ph) ph) (-> (-> ph ph) (-> ph ph))) merlem10 ax-mp ax-mp)
(-> (-> ph (-> ph ps)) (-> ph ps))
edit