Theorem olcs

Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis
olcs.1
\( \vdash \varphi \vee \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \)
Proof
olcs.1
orcoms _
\( \vdash \psi \vee \varphi \rightarrow \chi \)
orcs _