Theorem olcnd

A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2024.)

Hypotheses
olcnd.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
olcnd.2
\( \vdash \varphi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
olcnd.2
\( \vdash \varphi \rightarrow \neg \chi \)
olcnd.1
ord _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
mt3d l0 _