Description: Theorem 19.38 of Margaris p. 90. The converse holds under nonfreeness conditions, see 19.38a and 19.38b . (Contributed by NM, 12Mar1993) Allow a shortening of 19.21t . (Revised by Wolf Lammen, 2Jan2018)
Ref  Expression  

Assertion  19.38   ( ( E. x ph > A. x ps ) > A. x ( ph > ps ) ) 
Step  Hyp  Ref  Expression 

1  alnex   ( A. x . ph <> . E. x ph ) 

2  pm2.21   ( . ph > ( ph > ps ) ) 

3  2  alimi   ( A. x . ph > A. x ( ph > ps ) ) 
4  1 3  sylbir   ( . E. x ph > A. x ( ph > ps ) ) 
5  ala1   ( A. x ps > A. x ( ph > ps ) ) 

6  4 5  ja   ( ( E. x ph > A. x ps ) > A. x ( ph > ps ) ) 