Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23Jan1993) (Revised by Mario Carneiro, 24Sep2016) (Proof shortened by Wolf Lammen, 12Jan2018)
Ref  Expression  

Hypotheses  exlimd.1   F/ x ph 

exlimd.2   F/ x ch 

exlimd.3   ( ph > ( ps > ch ) ) 

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

1  exlimd.1   F/ x ph 

2  exlimd.2   F/ x ch 

3  exlimd.3   ( ph > ( ps > ch ) ) 

4  1 3  eximd   ( ph > ( E. x ps > E. x ch ) ) 
5  2  19.9   ( E. x ch <> ch ) 
6  4 5  syl6ib   ( ph > ( E. x ps > ch ) ) 