orim2d Show Code edit
# Disjoin antecedents and consequents in a deduction.
## Add disjunct to antecedent and consequent
thm (orim2d () (orim1d.1 (-> ph (-> ps ch))) (-> ph (-> (\/ th ps) (\/ th ch))) ph th idd orim1d.1 orim12d)
(-> ph (-> (\/ th ps) (\/ th ch)))
edit