orim2i Show Code edit
# Introduce disjunct to both sides of an implication.
## Introduce disjunct to both sides
thm (orim2i () (orim1i.1 (-> ph ps)) (-> (\/ ch ph) (\/ ch ps)) ch id orim1i.1 orim12i)
(-> (\/ ch ph) (\/ ch ps))
edit