Theorem jarli

Inference associated with jarl. Partial converse of ja (the other partial converse being jarri ). (Contributed by Wolf Lammen, 4-Oct-2013.)

Hypothesis
jarli.1
\( \vdash (\varphi \rightarrow \psi) \rightarrow \chi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \chi \)
Proof
l0
pm2.21
\( \vdash \neg \varphi \rightarrow \varphi \rightarrow \psi \)
jarli.1
\( \vdash (\varphi \rightarrow \psi) \rightarrow \chi \)
syl l0 _