imbi1d Show Code edit
# Deduction adding a consequent to both sides of a logical equivalence.
## Add a consequent to both sides
thm (imbi1d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (-> ps th) (-> ch th))) bid.1 notbid (-. th) imbi2d ps th con34b ch th con34b 3bitr4g)
(-> ph (<-> (-> ps th) (-> ch th)))
edit