Theorem albii

Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis
albii.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \forall x \, \varphi \leftrightarrow \forall x \, \psi \)
Proof
l0
albi
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\forall x \, \varphi \leftrightarrow \forall x \, \psi) \)
albii.1
\( \vdash \varphi \leftrightarrow \psi \)
mpg l0 _