Theorem nsyl5

A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)

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