Theorem 19.41

Theorem 19.41 of [Margaris] p. 90. See 19.41v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)

Hypothesis
19.41.1
\( \vdash \Finv x \, \psi \)
Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \exists x \, \varphi \wedge \psi \)
Proof
l0
19.40
\( \vdash \exists x \, (\varphi \wedge \psi) \rightarrow \exists x \, \varphi \wedge \exists x \, \psi \)
19.41.1
19.9 _
anbi2i _
\( \vdash \exists x \, \varphi \wedge \exists x \, \psi \leftrightarrow \exists x \, \varphi \wedge \psi \)
l4
sylib l0 _
l5
19.41.1
pm3.21
eximd l5 _
impcom _
impbii l4 _