Theorem tbwsyl

Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
tbwsyl.1
\( \vdash \varphi \rightarrow \psi \)
tbwsyl.2
\( \vdash \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
tbwsyl.2
\( \vdash \psi \rightarrow \chi \)
l1
tbwsyl.1
\( \vdash \varphi \rightarrow \psi \)
tbw-ax1
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l1 _
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _