Theorem impsingle-step4
Derivation of impsingle-step4 from [ax-mp] and impsingle. It is used
as a lemma in proofs of imim1 and peirce from impsingle. It is
Step 4 in Lukasiewicz, where it appears as 'CCCpqpCsp' using
parenthesis-free prefix notation. (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 \chi \rightarrow \varphi \)
Proof
l0
impsingle
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l1
impsingle
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
l2
impsingle
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
impsingle
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \)
l4
ax-mp l2 _
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \)
impsingle
\( \vdash (((((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
ax-mp l4 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
ax-mp l1 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \chi \rightarrow \varphi \)
ax-mp l0 _