Description: Deduce that x is not free in ps in a context. (Contributed by Wolf Lammen, 16Sep2021)
Ref  Expression  

Hypothesis  nfd.1   ( ph > ( E. x ps > A. x ps ) ) 

Assertion  nfd   ( ph > F/ x ps ) 
Step  Hyp  Ref  Expression 

1  nfd.1   ( ph > ( E. x ps > A. x ps ) ) 

2  dfnf   ( F/ x ps <> ( E. x ps > A. x ps ) ) 

3  1 2  sylibr   ( ph > F/ x ps ) 