Theorem nfded2

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

	Ref	Expression
Hypotheses	nfded2.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfded2.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
	nfded2.3	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → 𝐶 = 𝐷 )
	nfded2.4	⊢ Ⅎ 𝑥 𝐶
Assertion	nfded2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		nfded2.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfded2.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		nfded2.3	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → 𝐶 = 𝐷 )
4		nfded2.4	⊢ Ⅎ 𝑥 𝐶
5		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
6		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐵
7	5 6	nfan	⊢ Ⅎ 𝑥 ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 )
8	7 3	nfceqdf	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → ( Ⅎ 𝑥 𝐶 ↔ Ⅎ 𝑥 𝐷 ) )
9	1 2 8	syl2anc	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝐶 ↔ Ⅎ 𝑥 𝐷 ) )
10	4 9	mpbii	⊢ ( 𝜑 → Ⅎ 𝑥 𝐷 )