Description: Theorem 19.22 of Margaris p. 90. (Contributed by NM, 10Jan1993) (Proof shortened by Wolf Lammen, 4Jul2014)
Ref  Expression  

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

1  id   ( ( ph > ps ) > ( ph > ps ) ) 

2  1  aleximi   ( A. x ( ph > ps ) > ( E. x ph > E. x ps ) ) 