Theorem dedhb

Description: A deduction theorem for converting the inference |- F/_ x A => |- ph into a closed theorem. Use nfa1 and nfab to eliminate the hypothesis of the substitution instance ps of the inference. For converting the inference form into a deduction form, abidnf is useful. (Contributed by NM, 8-Dec-2006)

	Ref	Expression
Hypotheses	dedhb.1	$$⊢A=\left\{z|\forall xz\in A\right\}\to \left(\phi \leftrightarrow \psi \right)$$
	dedhb.2	$$⊢\psi$$
Assertion	dedhb	$$⊢\underset{\_}{Ⅎ}xA\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		dedhb.1	$$⊢A=\left\{z|\forall xz\in A\right\}\to \left(\phi \leftrightarrow \psi \right)$$
2		dedhb.2	$$⊢\psi$$
3		abidnf	$$⊢\underset{\_}{Ⅎ}xA\to \left\{z|\forall xz\in A\right\}=A$$
4	3	eqcomd	$$⊢\underset{\_}{Ⅎ}xA\to A=\left\{z|\forall xz\in A\right\}$$
5	4 1	syl	$$⊢\underset{\_}{Ⅎ}xA\to \left(\phi \leftrightarrow \psi \right)$$
6	2 5	mpbiri	$$⊢\underset{\_}{Ⅎ}xA\to \phi$$