Theorem impsingle-step25
Derivation of impsingle-step25 from [ax-mp] and impsingle. It is used
as a lemma in the proof of imim1 from impsingle. It is Step 25 in
Lukasiewicz, where it appears as 'CCpqCCCprqq' 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 \psi) \rightarrow \psi \)
Proof
l0
impsingle-step22
\( \vdash (((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
impsingle-step20
\( \vdash ((((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow ((\psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
l2
ax-mp l0 _
\( \vdash ((\psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
impsingle-step8
\( \vdash (((\psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
l4
ax-mp l2 _
\( \vdash (\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
impsingle-step15
\( \vdash ((\varphi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi) \rightarrow (\varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi) \rightarrow \psi \)
ax-mp l4 _