Description: Deduction form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 27Apr1994) Remove dependencies on ax6 , ax7 . (Revised by Wolf Lammen, 4Dec2017)
Ref  Expression  

Hypothesis  exlimdv.1   ( ph > ( ps > ch ) ) 

Assertion  exlimdv   ( ph > ( E. x ps > ch ) ) 
Step  Hyp  Ref  Expression 

1  exlimdv.1   ( ph > ( ps > ch ) ) 

2  1  eximdv   ( ph > ( E. x ps > E. x ch ) ) 
3  ax5e   ( E. x ch > ch ) 

4  2 3  syl6   ( ph > ( E. x ps > ch ) ) 