Step |
Hyp |
Ref |
Expression |
1 |
|
ax5e |
|- ( E. x E. y ps -> E. y ps ) |
2 |
|
ax-5 |
|- ( ph -> A. y ph ) |
3 |
2
|
ax-gen |
|- A. x ( ph -> A. y ph ) |
4 |
|
bj-cbveximt |
|- ( 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 ) ) ) ) ) |
5 |
4
|
com3l |
|- ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( A. x ( ph -> A. y ph ) -> ( A. x E. y ch -> ( ( E. x E. y ps -> E. y ps ) -> ( E. x ph -> E. y ps ) ) ) ) ) |
6 |
5
|
com14 |
|- ( ( E. x E. y ps -> E. y ps ) -> ( A. x ( ph -> A. y ph ) -> ( A. x E. y ch -> ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( E. x ph -> E. y ps ) ) ) ) ) |
7 |
1 3 6
|
mp2 |
|- ( A. x E. y ch -> ( A. x A. y ( ch -> ( ph -> ps ) ) -> ( E. x ph -> E. y ps ) ) ) |