pm5.42 Show Code edit
# Theorem *5.42 of [bib/WhiteheadRussell] p. 125.
thm (pm5.42 () () (<-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch)))) ph ch ibar ps imbi2d pm5.74i)
(<-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch))))
edit