This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )