merlem13 Show Code edit
# Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem13 () () (-> (-> ph ps) (-> (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ps)) th ch (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) merlem12 th ch (-. (-. ph)) merlem12 (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) (-. (-. ph)) merlem5 ax-mp (-> (-. (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) (-. (-. ph))) (-> (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) ps) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) (-> th (-> (-. (-. ch)) ch)) merlem6 ax-mp (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) ps (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))) (-. ph) (-> (-> th (-> (-. (-. ch)) ch)) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) meredith ax-mp ax-mp (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))))) (-> ps ps) ph (-> (-> (-> ps ps) (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))))) ph) merlem6 ax-mp (-> (-> (-> ps ps) (-> (-. ph) (-. (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph)))))) ph) ph merlem11 ax-mp ps ps ph (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ph meredith ax-mp)
(-> (-> ph ps) (-> (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ps))
edit