Theorem nsyl2

A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)

Hypotheses
nsyl2.1
\( \vdash \varphi \rightarrow \neg \psi \)
nsyl2.2
\( \vdash \neg \chi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
nsyl2.1
\( \vdash \varphi \rightarrow \neg \psi \)
nsyl2.2
\( \vdash \neg \chi \rightarrow \psi \)
nsyl3 l0 _
con4i _