Step |
Hyp |
Ref |
Expression |
1 |
|
bj-exalim |
|- ( A. y ( ch -> ( ph -> ps ) ) -> ( E. y ch -> ( A. y ph -> E. y ps ) ) ) |
2 |
1
|
alimi |
|- ( A. x A. y ( ch -> ( ph -> ps ) ) -> A. x ( E. y ch -> ( A. y ph -> E. y ps ) ) ) |
3 |
|
bj-alexim |
|- ( A. x ( E. y ch -> ( A. y ph -> E. y ps ) ) -> ( A. x E. y ch -> ( E. x A. y ph -> E. x E. y ps ) ) ) |
4 |
2 3
|
syl |
|- ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( A. x E. y ch -> ( E. x A. y ph -> E. x E. y ps ) ) ) |
5 |
|
exim |
|- ( A. x ( ph -> A. y ph ) -> ( E. x ph -> E. x A. y ph ) ) |
6 |
|
imim2 |
|- ( ( E. x A. y ph -> E. x E. y ps ) -> ( ( E. x ph -> E. x A. y ph ) -> ( E. x ph -> E. x E. y ps ) ) ) |
7 |
|
imim1 |
|- ( ( E. x ph -> E. x E. y ps ) -> ( ( E. x E. y ps -> E. y ps ) -> ( E. x ph -> E. y ps ) ) ) |
8 |
5 6 7
|
syl56 |
|- ( ( E. x A. y ph -> E. x E. y ps ) -> ( A. x ( ph -> A. y ph ) -> ( ( E. x E. y ps -> E. y ps ) -> ( E. x ph -> E. y ps ) ) ) ) |
9 |
4 8
|
syl6com |
|- ( A. x E. y ch -> ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( A. x ( ph -> A. y ph ) -> ( ( E. x E. y ps -> E. y ps ) -> ( E. x ph -> E. y ps ) ) ) ) ) |