Theorem mpgbir

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	mpgbir.1	|- ( ph <-> A. x ps )
	mpgbir.2	|- ps
Assertion	mpgbir	|- ph

Proof

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