Theorem re1tbw2

tbw-ax2 rederived from merco2. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \)
Proof
l0
mercolem1
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
mercolem1
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
l2
ax-mp l0 _
\( \vdash \varphi \rightarrow \psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
mercolem6
\( \vdash (\varphi \rightarrow \psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi) \rightarrow \psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
l4
ax-mp l2 _
\( \vdash \psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
mercolem6
\( \vdash (\psi \rightarrow \varphi \rightarrow \psi \rightarrow \varphi) \rightarrow \varphi \rightarrow \psi \rightarrow \varphi \)
ax-mp l4 _