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	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfded.2	$$⊢\underset{\_}{Ⅎ}xA\to B=C$$
	nfded.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfded	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$

Proof

Step	Hyp	Ref	Expression
1		nfded.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfded.2	$$⊢\underset{\_}{Ⅎ}xA\to B=C$$
3		nfded.3	$$⊢\underset{\_}{Ⅎ}xB$$
4		nfnfc1	$$⊢Ⅎx\underset{\_}{Ⅎ}xA$$
5	4 2	nfceqdf	$$⊢\underset{\_}{Ⅎ}xA\to \left(\underset{\_}{Ⅎ}xB\leftrightarrow \underset{\_}{Ⅎ}xC\right)$$
6	1 5	syl	$$⊢\phi \to \left(\underset{\_}{Ⅎ}xB\leftrightarrow \underset{\_}{Ⅎ}xC\right)$$
7	3 6	mpbii	$$⊢\phi \to \underset{\_}{Ⅎ}xC$$