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