pm5.36 Show Code edit
# Theorem *5.36 of [bib/WhiteheadRussell] p. 125.
thm (pm5.36 () () (<-> (/\ ph (<-> ph ps)) (/\ ps (<-> ph ps))) (<-> ph ps) id pm5.32ri)
(<-> (/\ ph (<-> ph ps)) (/\ ps (<-> ph ps)))
edit