Theorem nfim1

Description: A closed form of nfim . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 2-Jan-2018) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

	Ref	Expression
Hypotheses	nfim1.1	|- F/ x ph
	nfim1.2	|- ( ph -> F/ x ps )
Assertion	nfim1	|- F/ x ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		nfim1.1	|- F/ x ph
2		nfim1.2	|- ( ph -> F/ x ps )
3		nf3	|- ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
4	1 3	mpbi	|- ( A. x ph \/ A. x -. ph )
5		nftht	|- ( A. x ph -> F/ x ph )
6	2	sps	|- ( A. x ph -> F/ x ps )
7	5 6	nfimd	|- ( A. x ph -> F/ x ( ph -> ps ) )
8		pm2.21	|- ( -. ph -> ( ph -> ps ) )
9	8	alimi	|- ( A. x -. ph -> A. x ( ph -> ps ) )
10		nftht	|- ( A. x ( ph -> ps ) -> F/ x ( ph -> ps ) )
11	9 10	syl	|- ( A. x -. ph -> F/ x ( ph -> ps ) )
12	7 11	jaoi	|- ( ( A. x ph \/ A. x -. ph ) -> F/ x ( ph -> ps ) )
13	4 12	ax-mp	|- F/ x ( ph -> ps )