Step 
Hyp 
Ref 
Expression 
1 

elisset 
 ( A e. V > E. z z = A ) 
2 

nfnfc1 
 F/ x F/_ x A 
3 

nfcvd 
 ( F/_ x A > F/_ x z ) 
4 

id 
 ( F/_ x A > F/_ x A ) 
5 
3 4

nfeqd 
 ( F/_ x A > F/ x z = A ) 
6 

eqeq1 
 ( z = x > ( z = A <> x = A ) ) 
7 
6

a1i 
 ( F/_ x A > ( z = x > ( z = A <> x = A ) ) ) 
8 
2 5 7

cbvexd 
 ( F/_ x A > ( E. z z = A <> E. x x = A ) ) 
9 
1 8

syl5ib 
 ( F/_ x A > ( A e. V > E. x x = A ) ) 
10 
9

ad2antrr 
 ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) ) > ( A e. V > E. x x = A ) ) 
11 
10

3impia 
 ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) /\ A e. V ) > E. x x = A ) 
12 

biimp 
 ( ( ph <> ps ) > ( ph > ps ) ) 
13 
12

imim2i 
 ( ( x = A > ( ph <> ps ) ) > ( x = A > ( ph > ps ) ) ) 
14 
13

com23 
 ( ( x = A > ( ph <> ps ) ) > ( ph > ( x = A > ps ) ) ) 
15 
14

imp 
 ( ( ( x = A > ( ph <> ps ) ) /\ ph ) > ( x = A > ps ) ) 
16 
15

alanimi 
 ( ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) > A. x ( x = A > ps ) ) 
17 

19.23t 
 ( F/ x ps > ( A. x ( x = A > ps ) <> ( E. x x = A > ps ) ) ) 
18 
17

adantl 
 ( ( F/_ x A /\ F/ x ps ) > ( A. x ( x = A > ps ) <> ( E. x x = A > ps ) ) ) 
19 
16 18

syl5ib 
 ( ( F/_ x A /\ F/ x ps ) > ( ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) > ( E. x x = A > ps ) ) ) 
20 
19

imp 
 ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) ) > ( E. x x = A > ps ) ) 
21 
20

3adant3 
 ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) /\ A e. V ) > ( E. x x = A > ps ) ) 
22 
11 21

mpd 
 ( ( ( F/_ x A /\ F/ x ps ) /\ ( A. x ( x = A > ( ph <> ps ) ) /\ A. x ph ) /\ A e. V ) > ps ) 