pm5.33 Show Code edit
# Theorem *5.33 of [bib/WhiteheadRussell] p. 125.
thm (pm5.33 () () (<-> (/\ ph (-> ps ch)) (/\ ph (-> (/\ ph ps) ch))) ph ps ibar ch imbi1d pm5.32i)
(<-> (/\ ph (-> ps ch)) (/\ ph (-> (/\ ph ps) ch)))
edit