Theorem impsingle-step20
Derivation of impsingle-step20 from [ax-mp] and impsingle. It is used
as a lemma in proofs of imim1 and peirce from impsingle. It is
Step 20 in Lukasiewicz, where it appears as 'CCCCrppCspCCCpqrCsp' 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 \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
Proof
l0
impsingle-step19
\( \vdash (((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
l1
impsingle
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l2
impsingle
\( \vdash (((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
l3
impsingle
\( \vdash (((\chi \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
impsingle-step8
\( \vdash ((((\chi \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
l5
ax-mp l3 _
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
impsingle
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
l7
ax-mp l5 _
\( \vdash (((((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
impsingle
\( \vdash ((((((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
l9
ax-mp l7 _
\( \vdash ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
impsingle
\( \vdash (((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
l11
ax-mp l9 _
\( \vdash ((((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi \)
impsingle
\( \vdash (((((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
ax-mp l11 _
\( \vdash ((((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
ax-mp l2 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi) \rightarrow ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
ax-mp l1 _
\( \vdash ((((\chi \rightarrow \psi) \rightarrow \theta) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
ax-mp l0 _