pm2.73 Show Code edit
# Theorem *2.73 of [bib/WhiteheadRussell] p. 108.
thm (pm2.73 () () (-> (-> ph ps) (-> (\/ (\/ ph ps) ch) (\/ ps ch))) ph ps pm2.621 ch orim1d)
(-> (-> ph ps) (-> (\/ (\/ ph ps) ch) (\/ ps ch)))
edit