Theorem minimp-pm2.43

Derivation of pm2.43 (also called "hilbert" or W) from [ax-mp] and minimp. It uses the classical derivation from [ax-1] and [ax-2] written DD22D21 in D-notation (see head comment for an explanation) and shortens the proof using mp2 (which only requires [ax-mp] ). (Contributed by BJ, 31-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
Proof
l0
minimp-ax2
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \)
l1
minimp-ax1
\( \vdash \varphi \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi \)
minimp-ax2
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi \)
l3
ax-mp l1 _
\( \vdash (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi \)
minimp-ax2
\( \vdash ((\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi) \rightarrow ((\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi \rightarrow \psi) \rightarrow \varphi \rightarrow \psi \)
mp2 l0 l3 _