pm2.85 Show Code edit
# Theorem *2.85 of [bib/WhiteheadRussell] p. 108.
thm (pm2.85 () () (-> (-> (\/ ph ps) (\/ ph ch)) (\/ ph (-> ps ch))) (\/ ph ps) (\/ ph ch) imor ph ps pm2.48 (\/ ph ch) orim1i sylbi ps ch imor ph orbi2i ph (-. ps) ch orordi bitr2i sylib)
(-> (-> (\/ ph ps) (\/ ph ch)) (\/ ph (-> ps ch)))
edit