Description: Theorem *11.341 in WhiteheadRussell p. 162. Theorem 19.18 of Margaris p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | 2exbi | |- ( A. x A. y ( ph <-> ps ) -> ( E. x E. y ph <-> E. x E. y ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbi | |- ( A. y ( ph <-> ps ) -> ( E. y ph <-> E. y ps ) ) |
|
2 | 1 | alimi | |- ( A. x A. y ( ph <-> ps ) -> A. x ( E. y ph <-> E. y ps ) ) |
3 | exbi | |- ( A. x ( E. y ph <-> E. y ps ) -> ( E. x E. y ph <-> E. x E. y ps ) ) |
|
4 | 2 3 | syl | |- ( A. x A. y ( ph <-> ps ) -> ( E. x E. y ph <-> E. x E. y ps ) ) |