Theorem mpgbi

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	mpgbi.1	$$⊢\forall x\phi \leftrightarrow \psi$$
	mpgbi.2	$$⊢\phi$$
Assertion	mpgbi	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		mpgbi.1	$$⊢\forall x\phi \leftrightarrow \psi$$
2		mpgbi.2	$$⊢\phi$$
3	2	ax-gen	$$⊢\forall x\phi$$
4	3 1	mpbi	$$⊢\psi$$