ax3 Show Code edit
# Standard propositional axiom derived from Lukasiewicz axioms.
thm (ax3 () () (-> (-> (-. ph) (-. ps)) (-> ps ph)) (-. ph) ps ph ph luklem2 ph (-> ps ph) luklem4 luklem1)
(-> (-> (-. ph) (-. ps)) (-> ps ph))
edit