Theorem imim1i

Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1. Its associated inference is syl. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis
imim1i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
imim1i.1
id
imim12i l0 _