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