Theorem nfimt

Closed form of nfim and nfimd. (Contributed by BJ, 20-Oct-2021.) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6-Jul-2022.)

Conclusion
\( \vdash \Finv x \, \varphi \wedge \Finv x \, \psi \rightarrow \Finv x \, (\varphi \rightarrow \psi) \)
Proof
l0
simpl
simpr
nfimd l0 _