# Used to rederive standard propositional axioms from Lukasiewicz'.

thm (luklem3 () () (-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch))) ph (-. th) luk-3 (-. ph) th ps ch luklem2 luklem1)