Theorem impsingle-peirce

Derivation of impsingle-peirce ( peirce) from [ax-mp] and impsingle. It is step 28 in Lukasiewicz. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
impsingle-step22
\( \vdash \varphi \rightarrow \varphi \)
impsingle-step25
\( \vdash (\varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
ax-mp l0 _