anbi1 Show Code edit
# Theorem *4.36 of [bib/WhiteheadRussell] p. 118.
## Add a conjunct to both sides
thm (anbi1 () () (-> (<-> ph ps) (<-> (/\ ph ch) (/\ ps ch))) (<-> ph ps) id ch anbi1d)
(-> (<-> ph ps) (<-> (/\ ph ch) (/\ ps ch)))
edit