pm2.3 Show Code edit
# Theorem *2.3 of [bib/WhiteheadRussell] p. 104.
thm (pm2.3 () () (-> (\/ ph (\/ ps ch)) (\/ ph (\/ ch ps))) ps ch pm1.4 ph orim2i)
(-> (\/ ph (\/ ps ch)) (\/ ph (\/ ch ps)))
edit