Theorem 19.28v

Version of 19.28 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.)

Conclusion
\( \vdash \forall x \, (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \forall x \, \psi \)
Proof
l0
19.26
\( \vdash \forall x \, (\varphi \wedge \psi) \leftrightarrow \forall x \, \varphi \wedge \forall x \, \psi \)
19.3v
\( \vdash \forall x \, \varphi \leftrightarrow \varphi \)
bianbi l0 _