Theorem tbw-ax1

The first 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 (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)

Proof

imim1