pm5.75 Show Code edit
# Theorem *5.75 of [bib/WhiteheadRussell] p. 126.
thm (pm5.75 () () (-> (/\ (-> ch (-. ps)) (<-> ph (\/ ps ch))) (<-> (/\ ph (-. ps)) ch)) ph (\/ ps ch) bi1 ph ps ch pm5.6 sylibr (-> ch (-. ps)) adantl ph (\/ ps ch) bi2 ch ps olc ph ps olc imim12i syl ch ps ph pm5.6 sylibr exp3a a2d impcom (-> ch (-. ps)) (<-> ph (\/ ps ch)) pm3.26 jcad impbid)
(-> (/\ (-> ch (-. ps)) (<-> ph (\/ ps ch))) (<-> (/\ ph (-. ps)) ch))
edit