Theorem imim21b

Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.)

Conclusion
\( \vdash (\psi \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \leftrightarrow \psi \rightarrow \chi \rightarrow \theta) \)
Proof
l0
bi2.04
\( \vdash (\varphi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \leftrightarrow \psi \rightarrow (\varphi \rightarrow \chi) \rightarrow \theta \)
pm5.5
imbi1d _
imim2i _
pm5.74d _
\( \vdash (\psi \rightarrow \varphi) \rightarrow (\psi \rightarrow (\varphi \rightarrow \chi) \rightarrow \theta \leftrightarrow \psi \rightarrow \chi \rightarrow \theta) \)
bitrid l0 _