Metamath Proof Explorer


Theorem 2alanimi

Description: Removes two universal quantifiers from a statement. (Contributed by Andrew Salmon, 24-May-2011)

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

Proof

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