Theorem imimorb

Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)

Conclusion
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \vee \chi \)
Proof
l0
bi2.04
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \leftrightarrow \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
dfor2
imbi2i _
\( \vdash \varphi \rightarrow \psi \vee \chi \leftrightarrow \varphi \rightarrow (\psi \rightarrow \chi) \rightarrow \chi \)
bitr4i l0 _