merlem12 Show Code edit
# Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
thm (merlem12 () () (-> (-> (-> th (-> (-. (-. ch)) ch)) ph) ph) ch ch merlem5 ch (-> (-. (-. ch)) ch) th merlem2 ax-mp (-> th (-> (-. (-. ch)) ch)) ph (-> (-> th (-> (-. (-. ch)) ch)) ph) merlem4 ax-mp (-> (-> th (-> (-. (-. ch)) ch)) ph) ph merlem11 ax-mp)
(-> (-> (-> th (-> (-. (-. ch)) ch)) ph) ph)
edit