Theorem jarr

Elimination of a nested antecedent. Sometimes called "Syll-Simp" since it is a syllogism applied to [ax-1] ("Simplification"). (Contributed by Wolf Lammen, 9-May-2013.)

Conclusion

\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \psi \rightarrow \chi \)

Proof

ax-1

imim1i _