Theorem mpgbi

Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)

Hypotheses
mpgbi.1
\( \vdash \forall x \, \varphi \leftrightarrow \psi \)
mpgbi.2
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \)
Proof
mpgbi.2
l1
ax-gen _
\( \vdash \forall x \, \varphi \)
mpgbi.1
\( \vdash \forall x \, \varphi \leftrightarrow \psi \)
mpbi l1 _