ax2 Show Code edit
# Standard propositional axiom derived from Lukasiewicz axioms.
thm (ax2 () () (-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch))) ph ps ch luklem7 ps (-> ph ch) ph luklem8 ph ch luklem6 (-> ph (-> ph ch)) (-> ph ch) (-> ph ps) luklem8 ax-mp luklem1 luklem1)
(-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
edit