pm2.82 Show Code edit
# Theorem *2.82 of [bib/WhiteheadRussell] p. 108.
thm (pm2.82 () () (-> (\/ (\/ ph ps) ch) (-> (\/ (\/ ph (-. ch)) th) (\/ (\/ ph ps) th))) (\/ ph ps) (\/ ph (-. ch)) ax-1 ch ps pm2.24 ph orim2d jaoi th orim1d)
(-> (\/ (\/ ph ps) ch) (-> (\/ (\/ ph (-. ch)) th) (\/ (\/ ph ps) th)))
edit