Theorem retbwax4

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

Conclusion
\( \vdash \bot \rightarrow \varphi \)
Proof
l0
merco1lem1
\( \vdash \varphi \rightarrow \bot \rightarrow \varphi \)
merco1lem1
\( \vdash (\varphi \rightarrow \bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l0 _