orim12d Show Code edit
# Disjoin antecedents and consequents in a deduction.
## Join antecedents and consequents
thm (orim12d () (orim12d.1 (-> ph (-> ps ch)) orim12d.2 (-> ph (-> th ta))) (-> ph (-> (\/ ps th) (\/ ch ta))) ps ch th ta pm3.48 orim12d.1 orim12d.2 sylanc)
(-> ph (-> (\/ ps th) (\/ ch ta)))
edit