Description: Theorem *11.34 in WhiteheadRussell p. 162. Theorem 19.22 of Margaris p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | 2exim | |- ( A. x A. y ( ph -> ps ) -> ( E. x E. y ph -> E. x E. y ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exim | |- ( A. y ( ph -> ps ) -> ( E. y ph -> E. y ps ) ) |
|
2 | 1 | aleximi | |- ( A. x A. y ( ph -> ps ) -> ( E. x E. y ph -> E. x E. y ps ) ) |