Theorem mpgbi

Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994) (Proof shortened by Stefan Allan, 28-Oct-2008)

	Ref	Expression
Hypotheses	mpgbi.1	|- ( A. x ph <-> ps )
	mpgbi.2	|- ph
Assertion	mpgbi	|- ps

Proof

Step	Hyp	Ref	Expression
1		mpgbi.1	|- ( A. x ph <-> ps )
2		mpgbi.2	|- ph
3	2	ax-gen	|- A. x ph
4	3 1	mpbi	|- ps