Theorem bj-nfimt

Description: Closed form of nfim and curried (exported) form of nfimt . (Contributed by BJ, 20-Oct-2021) Proof should not use 19.35 . (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nfimt	|- ( F/ x ph -> ( F/ x ps -> F/ x ( ph -> ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( F/ x ph -> F/ x ph )
2	1	nfrd	|- ( F/ x ph -> ( E. x ph -> A. x ph ) )
3		bj-eximcom	|- ( E. x ( ph -> ps ) -> ( A. x ph -> E. x ps ) )
4	2 3	syl9	|- ( F/ x ph -> ( E. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) ) )
5		id	|- ( F/ x ps -> F/ x ps )
6	5	nfrd	|- ( F/ x ps -> ( E. x ps -> A. x ps ) )
7	6	imim2d	|- ( F/ x ps -> ( ( E. x ph -> E. x ps ) -> ( E. x ph -> A. x ps ) ) )
8		19.38	|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
9	7 8	syl6	|- ( F/ x ps -> ( ( E. x ph -> E. x ps ) -> A. x ( ph -> ps ) ) )
10	4 9	syl9	|- ( F/ x ph -> ( F/ x ps -> ( E. x ( ph -> ps ) -> A. x ( ph -> ps ) ) ) )
11		df-nf	|- ( F/ x ( ph -> ps ) <-> ( E. x ( ph -> ps ) -> A. x ( ph -> ps ) ) )
12	10 11	imbitrrdi	|- ( F/ x ph -> ( F/ x ps -> F/ x ( ph -> ps ) ) )