Theorem albi

Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.)

Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \rightarrow (\forall x \, \varphi \leftrightarrow \forall x \, \psi) \)
Proof
biimp
l1
al2imi _
biimpr
al2imi _
impbid l1 _