luklem5 Show Code edit
# Used to rederive standard propositional axioms from Lukasiewicz'.
thm (luklem5 () () (-> ph (-> ps ph)) ph ph ph ps luklem3 ph (-> ps ph) luklem4 luklem1)
(-> ph (-> ps ph))
edit