Theorem nfded

Description: A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., ( F/_ x A -> U. { y | A. x y e. A } = U. A ) ) that starts from abidnf . The last is assigned to the inference form (e.g., F/_ x U. { y | A. x y e. A } ) whose hypothesis is satisfied using nfaba1 . (Contributed by NM, 19-Nov-2020)

	Ref	Expression
Hypotheses	nfded.1	|- ( ph -> F/_ x A )
	nfded.2	|- ( F/_ x A -> B = C )
	nfded.3	|- F/_ x B
Assertion	nfded	|- ( ph -> F/_ x C )

Proof

Step	Hyp	Ref	Expression
1		nfded.1	|- ( ph -> F/_ x A )
2		nfded.2	|- ( F/_ x A -> B = C )
3		nfded.3	|- F/_ x B
4		nfnfc1	|- F/ x F/_ x A
5	4 2	nfceqdf	|- ( F/_ x A -> ( F/_ x B <-> F/_ x C ) )
6	1 5	syl	|- ( ph -> ( F/_ x B <-> F/_ x C ) )
7	3 6	mpbii	|- ( ph -> F/_ x C )