Theorem impsingle-imim1
Derivation of impsingle-imim1 ( imim1) from [ax-mp] and impsingle.
It is step 29 in Lukasiewicz. (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 \varphi \rightarrow \chi \)
Proof
l0
impsingle-step21
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
impsingle-step25
\( \vdash (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
impsingle-step25
\( \vdash ((\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
l3
ax-mp l1 _
\( \vdash (((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
impsingle-step21
\( \vdash ((((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l3 _
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _