Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12Aug2020)
Ref  Expression  

Hypotheses  spcedv.1   ( ph > X e. _V ) 

spcedv.2   ( ph > ch ) 

spcedv.3   ( x = X > ( ps <> ch ) ) 

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

1  spcedv.1   ( ph > X e. _V ) 

2  spcedv.2   ( ph > ch ) 

3  spcedv.3   ( x = X > ( ps <> ch ) ) 

4  3  spcegv   ( X e. _V > ( ch > E. x ps ) ) 
5  1 2 4  sylc   ( ph > E. x ps ) 