Theorem albiim

Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.)

Conclusion
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \leftrightarrow \forall x \, (\varphi \rightarrow \psi) \wedge \forall x \, (\psi \rightarrow \varphi) \)
Proof
dfbi2
l1
albii _
\( \vdash \forall x \, (\varphi \leftrightarrow \psi) \leftrightarrow \forall x \, ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \)
19.26
\( \vdash \forall x \, ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) \leftrightarrow \forall x \, (\varphi \rightarrow \psi) \wedge \forall x \, (\psi \rightarrow \varphi) \)
bitri l1 _