Theorem
orim2d
Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
Hypothesis
orim1d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \theta \vee \psi \rightarrow \theta \vee \chi \)
Proof
l0
idd
orim1d.1
orim12d
l0
_
This is the content in the right pane.