Description: If in a context x is not free in ps and ch , then it is not free in ( ps > ch ) . Deduction form of nfim . (Contributed by Mario Carneiro, 24Sep2016) (Proof shortened by Wolf Lammen, 30Dec2017) dfnf changed. (Revised by Wolf Lammen, 18Sep2021) Eliminate curried form of nfimt . (Revised by Wolf Lammen, 10Jul2022)
Ref  Expression  

Hypotheses  nfimd.1   ( ph > F/ x ps ) 

nfimd.2   ( ph > F/ x ch ) 

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

1  nfimd.1   ( ph > F/ x ps ) 

2  nfimd.2   ( ph > F/ x ch ) 

3  19.35   ( E. x ( ps > ch ) <> ( A. x ps > E. x ch ) ) 

4  3  biimpi   ( E. x ( ps > ch ) > ( A. x ps > E. x ch ) ) 
5  1  nfrd   ( ph > ( E. x ps > A. x ps ) ) 
6  2  nfrd   ( ph > ( E. x ch > A. x ch ) ) 
7  5 6  imim12d   ( ph > ( ( A. x ps > E. x ch ) > ( E. x ps > A. x ch ) ) ) 
8  19.38   ( ( E. x ps > A. x ch ) > A. x ( ps > ch ) ) 

9  4 7 8  syl56   ( ph > ( E. x ( ps > ch ) > A. x ( ps > ch ) ) ) 
10  9  nfd   ( ph > F/ x ( ps > ch ) ) 