pm2.48 Show Code edit
# Theorem *2.48 of [bib/WhiteheadRussell] p. 107.
thm (pm2.48 () () (-> (-. (\/ ph ps)) (\/ ph (-. ps))) ph ps pm2.46 ph olcd)
(-> (-. (\/ ph ps)) (\/ ph (-. ps)))
edit