Theorem jarri

Inference associated with jarr. Partial converse of ja (the other partial converse being jarli ). (Contributed by Wolf Lammen, 20-Sep-2013.)

Hypothesis
jarri.1
\( \vdash (\varphi \rightarrow \psi) \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \)
Proof
l0
ax-1
\( \vdash \psi \rightarrow \varphi \rightarrow \psi \)
jarri.1
\( \vdash (\varphi \rightarrow \psi) \rightarrow \chi \)
syl l0 _