Theorem mprg

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

	Ref	Expression
Hypotheses	mprg.1	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝜓 )
	mprg.2	⊢ ( 𝑥 ∈ 𝐴 → 𝜑 )
Assertion	mprg	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		mprg.1	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝜓 )
2		mprg.2	⊢ ( 𝑥 ∈ 𝐴 → 𝜑 )
3	2	rgen	⊢ ∀ 𝑥 ∈ 𝐴 𝜑
4	3 1	ax-mp	⊢ 𝜓