bimsc1 Show Code edit
## Removal of conjunct from one side of an equivalence
thm (bimsc1 () () (-> (/\ (-> ph ps) (<-> ch (/\ ps ph))) (<-> ch ph)) (<-> ch (/\ ps ph)) id ph ps pm4.71r biimpi bicomd sylan9bbr)
(-> (/\ (-> ph ps) (<-> ch (/\ ps ph))) (<-> ch ph))
edit