Theorem pm2.65d

Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)

Hypotheses
pm2.65d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
pm2.65d.2
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
pm2.65d.2
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \)
pm2.65d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
nsyld l0 _
pm2.01d _