orim12i Show Code edit
# Disjoin antecedents and consequents of two premises.
## Join antecedents and consequents
thm (orim12i () (orim12i.1 (-> ph ps) orim12i.2 (-> ch th)) (-> (\/ ph ch) (\/ ps th)) orim12i.1 con3i orim12i.2 con3i anim12i con3i ph ch oran ps th oran 3imtr4i)
(-> (\/ ph ch) (\/ ps th))
edit