Theorem mprg

Description: Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		mprg.1	|- ( A. x e. A ph -> ps )
2		mprg.2	|- ( x e. A -> ph )
3	2	rgen	|- A. x e. A ph
4	3 1	ax-mp	|- ps