Theorem 19.27v

Version of 19.27 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.)

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