Step |
Hyp |
Ref |
Expression |
1 |
|
ax6ev |
|- E. x x = y |
2 |
|
exim |
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( E. x x = y -> E. x ( ph -> ps ) ) ) |
3 |
1 2
|
mpi |
|- ( A. x ( x = y -> ( ph -> ps ) ) -> E. x ( ph -> ps ) ) |
4 |
|
19.35 |
|- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) ) |
5 |
3 4
|
sylib |
|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ph -> E. x ps ) ) |
6 |
|
19.9t |
|- ( F/ x ps -> ( E. x ps <-> ps ) ) |
7 |
6
|
biimpd |
|- ( F/ x ps -> ( E. x ps -> ps ) ) |
8 |
5 7
|
sylan9r |
|- ( ( F/ x ps /\ A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. x ph -> ps ) ) |