pm5.14 Show Code edit
# Theorem *5.14 of [bib/WhiteheadRussell] p. 123.
thm (pm5.14 () () (\/ (-> ph ps) (-> ps ch)) ps ph ax-1 con3i ch pm2.21d orri)
(\/ (-> ph ps) (-> ps ch))
edit