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 = { z | A. x z e. A } -> ( ph <-> ps ) )
	dedhb.2	|- ps
Assertion	dedhb	|- ( F/_ x A -> ph )

Proof

Step	Hyp	Ref	Expression
1		dedhb.1	|- ( A = { z | A. x z e. A } -> ( ph <-> ps ) )
2		dedhb.2	|- ps
3		abidnf	|- ( F/_ x A -> { z | A. x z e. A } = A )
4	3	eqcomd	|- ( F/_ x A -> A = { z | A. x z e. A } )
5	4 1	syl	|- ( F/_ x A -> ( ph <-> ps ) )
6	2 5	mpbiri	|- ( F/_ x A -> ph )