luklem3 Show Code edit
# Used to rederive standard propositional axioms from Lukasiewicz'.
thm (luklem3 () () (-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch))) ph (-. th) luk-3 (-. ph) th ps ch luklem2 luklem1)
(-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch)))
edit