Theorem
nsyl3
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
Hypotheses
nsyl3.1
\( \vdash \varphi \rightarrow \neg \psi \)
nsyl3.2
\( \vdash \chi \rightarrow \psi \)
Conclusion
\( \vdash \chi \rightarrow \neg \varphi \)
Proof
l0
nsyl3.2
\( \vdash \chi \rightarrow \psi \)
nsyl3.1
a1i
_
\( \vdash \chi \rightarrow \varphi \rightarrow \neg \psi \)
mt2d
l0
_
This is the content in the right pane.