Theorem mpgbir

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

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