Theorem jcnd

Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.)

Hypotheses
jcnd.1
\( \vdash \varphi \rightarrow \psi \)
jcnd.2
\( \vdash \varphi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg (\psi \rightarrow \chi) \)
Proof
l0
jcnd.1
\( \vdash \varphi \rightarrow \psi \)
l1
jcnd.2
\( \vdash \varphi \rightarrow \neg \chi \)
jcn
\( \vdash \psi \rightarrow \neg \chi \rightarrow \neg (\psi \rightarrow \chi) \)
sylc l0 l1 _