merlem5 Show Code edit
# Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem5 () () (-> (-> ph ps) (-> (-. (-. ph)) ps)) ps ps ps ps ps meredith ps ps ps (-. (-. ph)) ph meredith (-> ph ps) (-. ph) ps (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))) merlem1 (-> (-> (-> (-> ph ps) (-> (-. (-. ph)) ps)) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps))))) (-> (-. ph) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))))) ph (-> (-> (-> ps ps) (-> (-. ps) (-. (-. (-. ph))))) ps) merlem4 ax-mp (-> (-> ph ps) (-> (-. (-. ph)) ps)) (-. (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps)))) ph (-> (-> (-> (-> (-> ps ps) (-> (-. ps) (-. ps))) ps) ps) (-> (-> ps ps) (-> ps ps))) (-> (-> (-> (-> ps ps) (-> (-. ps) (-. (-. (-. ph))))) ps) ph) meredith ax-mp ax-mp ax-mp)
(-> (-> ph ps) (-> (-. (-. ph)) ps))
edit