luklem3
Show Code
edit
# 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
)
(-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch)))
edit