imbi2d Show Code edit
# Deduction adding an antecedent to both sides of a logical
# equivalence.
## Add an antecedent to both sides
thm (imbi2d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (-> th ps) (-> th ch))) bid.1 th a1d pm5.74d)
(-> ph (<-> (-> th ps) (-> th ch)))
edit