baib Show Code edit
## Move conjunction outside biconditional
thm (baib () (baib.1 (<-> ph (/\ ps ch))) (-> ps (<-> ph ch)) ps ch ibar baib.1 syl6rbbr)
(-> ps (<-> ph ch))
edit