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