bibi1d Show Code edit
# Deduction adding a biconditional to the right in an equivalence.
## Add a biconditional to both sides
thm (bibi1d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (<-> ps th) (<-> ch th))) bid.1 th bibi2d ps th bicom ch th bicom 3bitr4g)
(-> ph (<-> (<-> ps th) (<-> ch th)))
edit