anbi2d Show Code edit
# Deduction adding a left conjunct to both sides of a logical
# equivalence.
## Add a conjunct to both sides
thm (anbi2d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (/\ th ps) (/\ th ch))) bid.1 biimpd th anim2d bid.1 biimprd th anim2d impbid)
(-> ph (<-> (/\ th ps) (/\ th ch)))
edit