Theorem tbw-ax3

The third of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \rightarrow \psi) \rightarrow \varphi) \rightarrow \varphi \)
Proof
peirce