Theorem orcnd

A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.)

Hypotheses
orcnd.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
orcnd.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
orcnd.1
l1
orcomd _
\( \vdash \varphi \rightarrow \chi \vee \psi \)
orcnd.2
\( \vdash \varphi \rightarrow \neg \psi \)
olcnd l1 _