Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv ). (Contributed by Mario Carneiro, 15Jun2016)
Ref  Expression  

Hypotheses  exlimddv.1   ( ph > E. x ps ) 

exlimddv.2   ( ( ph /\ ps ) > ch ) 

Assertion  exlimddv   ( ph > ch ) 
Step  Hyp  Ref  Expression 

1  exlimddv.1   ( ph > E. x ps ) 

2  exlimddv.2   ( ( ph /\ ps ) > ch ) 

3  2  ex   ( ph > ( ps > ch ) ) 
4  3  exlimdv   ( ph > ( E. x ps > ch ) ) 
5  1 4  mpd   ( ph > ch ) 