Theorem imim2i

Inference adding common antecedents in an implication. Inference associated with imim2. Its associated inference is syl. (Contributed by NM, 28-Dec-1992.)

Hypothesis
imim2i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash (\chi \rightarrow \varphi) \rightarrow \chi \rightarrow \psi \)
Proof
imim2i.1
a1i _
a2i _