bitr Show Code edit
# Theorem *4.22 of [bib/WhiteheadRussell] p. 117.
## Transitive Property
## right('Transitive', '↔')
thm (bitr () () (-> (/\ (<-> ph ps) (<-> ps ch)) (<-> ph ch)) (<-> ph ps) id ch bibi1d biimpar)
(-> (/\ (<-> ph ps) (<-> ps ch)) (<-> ph ch))
edit