merlem1 Show Code edit
# Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
# (The step numbers refer to Meredith's original paper.)
thm (merlem1 () () (-> (-> (-> ch (-> (-. ph) ps)) ta) (-> ph ta)) (-. ph) ps (-> (-. ta) (-. ch)) (-. (-> (-. ph) ps)) ta meredith (-> (-. ph) ps) (-> (-. (-> (-. ta) (-. ch))) (-. (-. (-> (-. ph) ps)))) ta ch (-> (-> ta (-. ph)) (-> (-. (-> (-. ph) ps)) (-. ph))) meredith ax-mp ta (-. ph) (-> (-. ph) ps) ph (-> ch (-> (-. ph) ps)) meredith ax-mp)
(-> (-> (-> ch (-> (-. ph) ps)) ta) (-> ph ta))
edit