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