Metamath Proof Explorer


Theorem alanimi

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

Ref Expression
Hypothesis alanimi.1
|- ( ( ph /\ ps ) -> ch )
Assertion alanimi
|- ( ( A. x ph /\ A. x ps ) -> A. x ch )

Proof

Step Hyp Ref Expression
1 alanimi.1
 |-  ( ( ph /\ ps ) -> ch )
2 1 ex
 |-  ( ph -> ( ps -> ch ) )
3 2 al2imi
 |-  ( A. x ph -> ( A. x ps -> A. x ch ) )
4 3 imp
 |-  ( ( A. x ph /\ A. x ps ) -> A. x ch )