pm2.74 Show Code edit
# Theorem *2.74 of [bib/WhiteheadRussell] p. 108.
thm (pm2.74 () () (-> (-> ps ph) (-> (\/ (\/ ph ps) ch) (\/ ph ch))) ps ph orel2 ch orim1d ph ch orc (\/ (\/ ph ps) ch) a1d ja)
(-> (-> ps ph) (-> (\/ (\/ ph ps) ch) (\/ ph ch)))
edit