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