pm5.62 Show Code edit
# Theorem *5.62 of [bib/WhiteheadRussell] p. 125. (Contributed by Roy F.
# Longton, 21-Jun-2005.)
thm (pm5.62 () () (<-> (\/ (/\ ph ps) (-. ps)) (\/ ph (-. ps))) ph ps (-. ps) ordir ps exmid mpbiran2)
(<-> (\/ (/\ ph ps) (-. ps)) (\/ ph (-. ps)))
edit