pm2.63 Show Code edit
# Theorem *2.63 of [bib/WhiteheadRussell] p. 107.
thm (pm2.63 () () (-> (\/ ph ps) (-> (\/ (-. ph) ps) ps)) ph ps pm2.53 (\/ ph ps) ps idd jaod)
(-> (\/ ph ps) (-> (\/ (-. ph) ps) ps))
edit