pm5.12 Show Code edit
# Theorem *5.12 of [bib/WhiteheadRussell] p. 123.
thm (pm5.12 () () (\/ (-> ph ps) (-> ph (-. ps))) ph ps pm2.51 orri)
(\/ (-> ph ps) (-> ph (-. ps)))
edit