merlem7 Show Code edit
# Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his
# sole axiom.
thm (merlem7 () () (-> ph (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th))) (-> ps ch) th (-> (-> ch ta) (-> (-. th) (-. ps))) merlem4 (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th) (-> (-> ps ch) th) (-. ph) (-. ch) merlem6 ch ta th ps (-> (-> (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) (-. ph)) (-> (-. ch) (-. ph))) meredith ax-mp (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)) (-. ph) ch ph (-> ps ch) meredith ax-mp ax-mp)
(-> ph (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)))
edit