tbw-ax3 rederived from merco2. (Contributed by Anthony Hart,
16-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi \)
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
\( \vdash (((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
\( \vdash (((\varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \varphi \rightarrow \varphi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)