ax1 Show Code edit
# Standard propositional axiom derived from Lukasiewicz axioms.
thm (ax1 () () (-> ph (-> ps ph)) ph ps luklem5)
(-> ph (-> ps ph))
edit