Theorem minimp-ax1

Derivation of [ax-1] from [ax-mp] and minimp. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \)
Proof
l0
minimp-syllsimp
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \)
minimp-syllsimp
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l0 _