Theorem re1tbw4

tbw-ax4 rederived from merco2.

This theorem, along with re1tbw1, re1tbw2, and re1tbw3, shows that merco2, along with [ax-mp], can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \bot \rightarrow \varphi \)
Proof
l0
re1tbw3
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \)
l1
re1tbw2
\( \vdash \varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi \)
re1tbw1
\( \vdash (\varphi \rightarrow (\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
ax-mp l1 _
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \)
l4
ax-mp l0 _
\( \vdash \varphi \rightarrow \varphi \)
l5
re1tbw3
\( \vdash (((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
l6
re1tbw2
\( \vdash (\bot \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
re1tbw1
\( \vdash ((\bot \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow ((((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l6 _
\( \vdash ((((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
l9
ax-mp l5 _
\( \vdash (\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
l10
mercolem3
\( \vdash ((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
merco2
\( \vdash (((\bot \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow ((\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l10 _
\( \vdash ((\bot \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l9 _
\( \vdash (\varphi \rightarrow \varphi) \rightarrow (\varphi \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l4 _
\( \vdash (\varphi \rightarrow \varphi) \rightarrow \bot \rightarrow \varphi \)
ax-mp l4 _