pm5.31 Show Code edit
# Theorem *5.31 of [bib/WhiteheadRussell] p. 125.
thm (pm5.31 () () (-> (/\ ch (-> ph ps)) (-> ph (/\ ps ch))) ch ps pm3.21 ph imim2d imp)
(-> (/\ ch (-> ph ps)) (-> ph (/\ ps ch)))
edit