merlem9 Show Code edit
# Step 18 of Meredith's proof of Lukasiewicz axioms from his sole
# axiom.
thm (merlem9 () () (-> (-> (-> ph ps) (-> ch (-> th (-> ps ta)))) (-> et (-> ch (-> th (-> ps ta))))) (-> th (-> ps ta)) ch (-. et) (-. ps) merlem6 th (-> ps ta) (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et))) (-> (-. (-> (-. (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et)))) (-. th))) (-. ph)) merlem8 ax-mp ps ta (-> (-. (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et)))) (-. th)) ph (-> (-> (-> ch (-> th (-> ps ta))) (-. et)) (-> (-. ps) (-. et))) meredith ax-mp (-> ch (-> th (-> ps ta))) (-. et) ps et (-> ph ps) meredith ax-mp)
(-> (-> (-> ph ps) (-> ch (-> th (-> ps ta)))) (-> et (-> ch (-> th (-> ps ta)))))
edit