Theorem re1tbw1
tbw-ax1 rederived from merco2. (Contributed by Anthony Hart,
16-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
mercolem3
\( \vdash (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi \)
l1
mercolem8
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mercolem6
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l3
ax-mp l1 _
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mercolem3
\( \vdash ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l5
ax-mp l3 _
\( \vdash (\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l6
mercolem8
\( \vdash ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mercolem6
\( \vdash (((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l6 _
\( \vdash ((\psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l5 _
\( \vdash ((\psi \rightarrow \chi) \rightarrow \psi \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l10
ax-mp l0 _
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mercolem6
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l12
ax-mp l10 _
\( \vdash (\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
mercolem6
\( \vdash ((\psi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l12 _