Theorem mprg

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

	Ref	Expression
Hypotheses	mprg.1	$$⊢\forall x\in A\phi \to \psi$$
	mprg.2	$$⊢x\in A\to \phi$$
Assertion	mprg	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		mprg.1	$$⊢\forall x\in A\phi \to \psi$$
2		mprg.2	$$⊢x\in A\to \phi$$
3	2	rgen	$$⊢\forall x\in A\phi$$
4	3 1	ax-mp	$$⊢\psi$$