luklem1 Show Code edit
# Used to rederive standard propositional axioms from Lukasiewicz'.
thm (luklem1 () (luklem1.1 (-> ph ps) luklem1.2 (-> ps ch)) (-> ph ch) luklem1.2 luklem1.1 ph ps ch luk-1 ax-mp ax-mp)
(-> ph ch)
edit