Theorem 19.42

Theorem 19.42 of [Margaris] p. 90. See 19.42v for a version requiring fewer axioms. See exan for an immediate version. (Contributed by NM, 18-Aug-1993.)

Hypothesis
19.42.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \exists x \, \psi \)
Proof
19.42.1
l1
19.41 _
\( \vdash \exists x \, (\psi \wedge \varphi) \leftrightarrow \exists x \, \psi \wedge \varphi \)
l2
exancom
\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\psi \wedge \varphi) \)
ancom
\( \vdash \varphi \wedge \exists x \, \psi \leftrightarrow \exists x \, \psi \wedge \varphi \)
3bitr4i l1 l2 _