nic-luk1 Show Code edit
# Proof of [[luk-1]] from [[nic-ax]] and [[nic-mp]] (and definitions
# [[nic-dfim]] and [[nic-dfneg]]). Note that the standard axioms [[ax-1]],
# [[ax-2]], and [[ax-3]] are proved from the Lukasiewicz axioms by theorems
# [[ax1]], [[ax2]], and [[ax3]]. (Contributed by Jeff Hoffman,
# 18-Nov-2007.)
thm (nic-luk1 () () (-> (-> ph ps) (-> (-> ps ch) (-> ph ch))) ph ps nic-dfim nic-bi2 ph ps ps ta (-/\ ch ch) nic-ax nic-isw2 nic-idel ph ch nic-dfim nic-bi1 nic-idbl (-/\ (-/\ ch ch) ps) nic-imp ps ch nic-dfim nic-bi2 ps (-/\ ch ch) nic-swap nic-ich (-/\ (-> ph ch) (-> ph ch)) nic-imp nic-ich nic-ich (-> ps ch) (-> ph ch) nic-dfim nic-bi1 nic-ich nic-ich (-> ph ps) (-> (-> ps ch) (-> ph ch)) nic-dfim nic-bi1 nic-mp)
(-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
edit