Theorem jc

Deduction joining the consequents of two premises. A deduction associated with pm3.2im. (Contributed by NM, 28-Dec-1992.)

Hypotheses
jc.1
\( \vdash \varphi \rightarrow \psi \)
jc.2
\( \vdash \varphi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \neg (\psi \rightarrow \neg \chi) \)
Proof
l0
jc.1
\( \vdash \varphi \rightarrow \psi \)
l1
jc.2
\( \vdash \varphi \rightarrow \chi \)
pm3.2im
\( \vdash \psi \rightarrow \chi \rightarrow \neg (\psi \rightarrow \neg \chi) \)
sylc l0 l1 _