Theorem retbwax3

tbw-ax3 rederived from merco1. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
retbwax2
\( \vdash \varphi \rightarrow \varphi \rightarrow \varphi \)
merco1lem7
\( \vdash (\varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
ax-mp l0 _