Derivation of impsingle-step19 from [ax-mp] and impsingle. It is used
as a lemma in proofs of imim1 and peirce from impsingle. It is
Step 19 in Lukasiewicz, where it appears as 'CCCCspqCrpCCCpqrCsp' 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 \theta \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
\( \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 \)
\( \vdash (((\theta \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \theta \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
\( \vdash ((((\theta \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi) \rightarrow \theta \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \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 \psi) \rightarrow \chi) \rightarrow \theta \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
\( \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 \psi) \rightarrow \chi) \rightarrow \theta \rightarrow \psi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)