bibi2d Show Code edit
# Deduction adding a biconditional to the left in an equivalence.
## Add a biconditional to both sides
thm (bibi2d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (<-> th ps) (<-> th ch))) bid.1 th imbi2d (-> ps th) anbi1d bid.1 th imbi1d (-> th ch) anbi2d bitrd th ps dfbi2 th ch dfbi2 3bitr4g)
(-> ph (<-> (<-> th ps) (<-> th ch)))
edit