pm5.55 Show Code edit
# Theorem *5.55 of [bib/WhiteheadRussell] p. 125.
thm (pm5.55 () () (\/ (<-> (\/ ph ps) ph) (<-> (\/ ph ps) ps)) ps ph pm5.13 ps ph pm4.72 ps ph orcom ph bibi2i ph (\/ ph ps) bicom 3bitri ph ps pm4.72 ps (\/ ph ps) bicom bitri orbi12i mpbi)
(\/ (<-> (\/ ph ps) ph) (<-> (\/ ph ps) ps))
edit