Derivation of impsingle-step21 from [ax-mp] and impsingle. It is used
as a lemma in the proof of imim1 from impsingle. It is Step 21 in
Lukasiewicz, where it appears as 'CCCCprqqCCqrCpr' 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 \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
\( \vdash ((\chi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
\( \vdash (((\chi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \chi) \rightarrow (\chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)