pm2.47 Show Code edit
# Theorem *2.47 of [bib/WhiteheadRussell] p. 107.
thm (pm2.47 () () (-> (-. (\/ ph ps)) (\/ (-. ph) ps)) ph ps pm2.45 ps orcd)
(-> (-. (\/ ph ps)) (\/ (-. ph) ps))
edit