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