Description: Closed form of nfim and nfimd . (Contributed by BJ, 20Oct2021) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6Jul2022)
Ref  Expression  

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

1  simpl   ( ( F/ x ph /\ F/ x ps ) > F/ x ph ) 

2  simpr   ( ( F/ x ph /\ F/ x ps ) > F/ x ps ) 

3  1 2  nfimd   ( ( F/ x ph /\ F/ x ps ) > F/ x ( ph > ps ) ) 