Theorem nsyl4

A negated syllogism inference. (Contributed by NM, 15-Feb-1996.)

Hypotheses
nsyl4.1
\( \vdash \varphi \rightarrow \psi \)
nsyl4.2
\( \vdash \neg \varphi \rightarrow \chi \)
Conclusion
\( \vdash \neg \chi \rightarrow \psi \)
Proof
nsyl4.2
l1
con1i _
\( \vdash \neg \chi \rightarrow \varphi \)
nsyl4.1
\( \vdash \varphi \rightarrow \psi \)
syl l1 _