pm2.75 Show Code edit
# Theorem *2.75 of [bib/WhiteheadRussell] p. 108.
thm (pm2.75 () () (-> (\/ ph ps) (-> (\/ ph (-> ps ch)) (\/ ph ch))) ph ch orc (\/ ph (-> ps ch)) a1d ps ch pm2.27 ph orim2d jaoi)
(-> (\/ ph ps) (-> (\/ ph (-> ps ch)) (\/ ph ch)))
edit