pm5.54 Show Code edit
# Theorem *5.54 of [bib/WhiteheadRussell] p. 125.
thm (pm5.54 () () (\/ (<-> (/\ ph ps) ph) (<-> (/\ ph ps) ps)) (/\ ph ps) ph pm5.1 anabss1 ps ph iba bicomd pm5.21ni orri)
(\/ (<-> (/\ ph ps) ph) (<-> (/\ ph ps) ps))
edit