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 ) |
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 ) |