bibi1 Show Code edit
# Theorem *4.86 of [bib/WhiteheadRussell] p. 122.
## Add a biconditional to both sides
thm (bibi1 () () (-> (<-> ph ps) (<-> (<-> ph ch) (<-> ps ch))) (<-> ph ps) id ch bibi1d)
(-> (<-> ph ps) (<-> (<-> ph ch) (<-> ps ch)))
edit