Theorem mopick2

"At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Conclusion
\( \vdash \exists^\ast x \, \varphi \wedge \exists x \, (\varphi \wedge \psi) \wedge \exists x \, (\varphi \wedge \chi) \rightarrow \exists x \, (\varphi \wedge \psi \wedge \chi) \)
Proof
l0
nfmo1
nfe1
l2
nfan l0 _
mopick
ancld _
l5
anim1d _
\( \vdash \exists^\ast x \, \varphi \wedge \exists x \, (\varphi \wedge \psi) \rightarrow \varphi \wedge \chi \rightarrow \varphi \wedge \psi \wedge \chi \)
df-3an
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge \chi \)
imbitrrdi l5 _
eximd l2 _
3impia _