pm2.64 Show Code edit
# Theorem *2.64 of [bib/WhiteheadRussell] p. 107.
thm (pm2.64 () () (-> (\/ ph ps) (-> (\/ ph (-. ps)) ph)) ph (\/ ph ps) ax-1 ps ph orel2 jaoi com12)
(-> (\/ ph ps) (-> (\/ ph (-. ps)) ph))
edit