orbi2d Show Code edit
# Deduction adding a left disjunct to both sides of a logical
# equivalence.
## Add a disjunct to both sides
thm (orbi2d () (bid.1 (-> ph (<-> ps ch))) (-> ph (<-> (\/ th ps) (\/ th ch))) bid.1 (-. th) imbi2d th ps df-or th ch df-or 3bitr4g)
(-> ph (<-> (\/ th ps) (\/ th ch)))
edit