Theorem impsingle-step18
Derivation of impsingle-step18 from [ax-mp] and impsingle. It is used
as a lemma in proofs of imim1 and peirce from impsingle. It is
Step 18 in Lukasiewicz, where it appears as 'CCCCrpCspCCCpqrtCuCCCpqrt'
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 \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \eta \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau \)
Proof
l0
impsingle
\( \vdash ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
l1
impsingle
\( \vdash (((\chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
impsingle-step8
\( \vdash ((((\chi \rightarrow \psi) \rightarrow \varphi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
l3
ax-mp l1 _
\( \vdash (((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
impsingle-step15
\( \vdash ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
ax-mp l3 _
\( \vdash (((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
l6
ax-mp l0 _
\( \vdash ((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi \)
impsingle
\( \vdash (((((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \chi \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow \chi \rightarrow \psi) \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau) \rightarrow \eta \rightarrow ((\psi \rightarrow \theta) \rightarrow \varphi) \rightarrow \tau \)
ax-mp l6 _