Theorem mpg

Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994)

	Ref	Expression
Hypotheses	mpg.1	$$⊢\forall x\phi \to \psi$$
	mpg.2	$$⊢\phi$$
Assertion	mpg	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		mpg.1	$$⊢\forall x\phi \to \psi$$
2		mpg.2	$$⊢\phi$$
3	2	ax-gen	$$⊢\forall x\phi$$
4	3 1	ax-mp	$$⊢\psi$$