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