pm5.17 Show Code edit
# Theorem *5.17 of [bib/WhiteheadRussell] p. 124.
thm (pm5.17 () () (<-> (/\ (\/ ph ps) (-. (/\ ph ps))) (<-> ph (-. ps))) ph ps orcom ps ph df-or bitri ph ps imnan bicomi anbi12i (-. ps) ph dfbi2 (-. ps) ph bicom 3bitr2i)
(<-> (/\ (\/ ph ps) (-. (/\ ph ps))) (<-> ph (-. ps)))
edit