nan Show Code edit
## Move a conjunct in and out of negation
thm (nan () () (<-> (-> ph (-. (/\ ps ch))) (-> (/\ ph ps) (-. ch))) ph ps (-. ch) impexp ps ch imnan ph imbi2i bitr2i)
(<-> (-> ph (-. (/\ ps ch))) (-> (/\ ph ps) (-. ch)))
edit