Theorem alanimi

Variant of al2imi with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)

Hypothesis
alanimi.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \forall x \, \varphi \wedge \forall x \, \psi \rightarrow \forall x \, \chi \)
Proof
alanimi.1
ex _
al2imi _
imp _