Theorem impsingle-ax1

Derivation of impsingle-ax1 ( [ax-1]) from [ax-mp] and impsingle. Lukasiewicz was used to construct this proof. Every formula corresponding to a detachment step was converted to its corresponding Metamath formula. mmj2 was used to unify each formula using [ax-mp], which in turn produced this proof. With extremely high confidence, this result shows that the Lukasiewicz proof of [ax-1] (step 27) is correct and that Metamath correctly verifies the proof. The same comments apply to the proofs that follow this one. (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 \)
Proof
l0
impsingle-step8
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
impsingle-step8
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l0 _