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	|- ( ph -> F/_ x A )
	nfded2.2	|- ( ph -> F/_ x B )
	nfded2.3	|- ( ( F/_ x A /\ F/_ x B ) -> C = D )
	nfded2.4	|- F/_ x C
Assertion	nfded2	|- ( ph -> F/_ x D )

Proof

Step	Hyp	Ref	Expression
1		nfded2.1	|- ( ph -> F/_ x A )
2		nfded2.2	|- ( ph -> F/_ x B )
3		nfded2.3	|- ( ( F/_ x A /\ F/_ x B ) -> C = D )
4		nfded2.4	|- F/_ x C
5		nfnfc1	|- F/ x F/_ x A
6		nfnfc1	|- F/ x F/_ x B
7	5 6	nfan	|- F/ x ( F/_ x A /\ F/_ x B )
8	7 3	nfceqdf	|- ( ( F/_ x A /\ F/_ x B ) -> ( F/_ x C <-> F/_ x D ) )
9	1 2 8	syl2anc	|- ( ph -> ( F/_ x C <-> F/_ x D ) )
10	4 9	mpbii	|- ( ph -> F/_ x D )