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	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfded.2	⊢ ( Ⅎ 𝑥 𝐴 → 𝐵 = 𝐶 )
	nfded.3	⊢ Ⅎ 𝑥 𝐵
Assertion	nfded	⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		nfded.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfded.2	⊢ ( Ⅎ 𝑥 𝐴 → 𝐵 = 𝐶 )
3		nfded.3	⊢ Ⅎ 𝑥 𝐵
4		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
5	4 2	nfceqdf	⊢ ( Ⅎ 𝑥 𝐴 → ( Ⅎ 𝑥 𝐵 ↔ Ⅎ 𝑥 𝐶 ) )
6	1 5	syl	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝐵 ↔ Ⅎ 𝑥 𝐶 ) )
7	3 6	mpbii	⊢ ( 𝜑 → Ⅎ 𝑥 𝐶 )