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	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfded2.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
	nfded2.3	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to C=D$$
	nfded2.4	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	nfded2	$$⊢\phi \to \underset{\_}{Ⅎ}xD$$

Proof

Step	Hyp	Ref	Expression
1		nfded2.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfded2.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
3		nfded2.3	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to C=D$$
4		nfded2.4	$$⊢\underset{\_}{Ⅎ}xC$$
5		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xA$$
6		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xB$$
7	5 6	nfan	$$⊢Ⅎx\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)$$
8	7 3	nfceqdf	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to \left(\underset{\_}{Ⅎ}xC\leftrightarrow \underset{\_}{Ⅎ}xD\right)$$
9	1 2 8	syl2anc	$$⊢\phi \to \left(\underset{\_}{Ⅎ}xC\leftrightarrow \underset{\_}{Ⅎ}xD\right)$$
10	4 9	mpbii	$$⊢\phi \to \underset{\_}{Ⅎ}xD$$