anbi1d Show Code edit
# Deduction adding a right conjunct to both sides of a logical
# equivalence.
## Add a conjunct to both sides
thm (anbi1d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (/\ ps th) (/\ ch th))) bid.1 th anbi2d ps th ancom ch th ancom 3bitr4g)
(-> ph (<-> (/\ ps th) (/\ ch th)))
edit