pm3.3 Show Code edit
# Theorem *3.3 (Exp) of [bib/WhiteheadRussell] p. 112.
## Export Theorem Collary
thm (pm3.3 () () (-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) ph ps ch impexp biimpi)
(-> (-> (/\ ph ps) ch) (-> ph (-> ps ch)))
edit