Step |
Hyp |
Ref |
Expression |
1 |
|
biimpr |
|- ( ( ph <-> ps ) -> ( ps -> ph ) ) |
2 |
1
|
imim2i |
|- ( ( x = A -> ( ph <-> ps ) ) -> ( x = A -> ( ps -> ph ) ) ) |
3 |
2
|
com23 |
|- ( ( x = A -> ( ph <-> ps ) ) -> ( ps -> ( x = A -> ph ) ) ) |
4 |
3
|
alimi |
|- ( A. x ( x = A -> ( ph <-> ps ) ) -> A. x ( ps -> ( x = A -> ph ) ) ) |
5 |
|
19.21t |
|- ( F/ x ps -> ( A. x ( ps -> ( x = A -> ph ) ) <-> ( ps -> A. x ( x = A -> ph ) ) ) ) |
6 |
4 5
|
imbitrid |
|- ( F/ x ps -> ( A. x ( x = A -> ( ph <-> ps ) ) -> ( ps -> A. x ( x = A -> ph ) ) ) ) |
7 |
6
|
imp |
|- ( ( F/ x ps /\ A. x ( x = A -> ( ph <-> ps ) ) ) -> ( ps -> A. x ( x = A -> ph ) ) ) |