Theorem peirceroll

Over minimal implicational calculus, Peirce's axiom peirce implies an axiom sometimes called "Roll", \( ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\chi \rightarrow \varphi) \rightarrow \varphi \), of which looinv is a special instance. The converse also holds: substitute \( \varphi \rightarrow \psi \) for \( \chi \) in Roll and use id and [ax-mp]. (Contributed by BJ, 15-Jun-2021.)

Conclusion
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\chi \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
imim1
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow (\chi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \)
id
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
syl9r l0 _