Derivation of impsingle-step22 from [ax-mp] and impsingle. It is used
as a lemma in proofs of imim1 and peirce from impsingle. It is
Step 22 in Lukasiewicz, where it appears as 'Cpp' using parenthesis-free
prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado,
2-Aug-2023.) (Proof modification is discouraged.)
(New usage is discouraged.)
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \)
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)