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