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