Theorem 2eu2ex

Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)

Conclusion
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists x \, \exists y \, \varphi \)
Proof
l0
euex
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists x \, \exists{!} y \, \varphi \)
euex
eximi _
\( \vdash \exists x \, \exists{!} y \, \varphi \rightarrow \exists x \, \exists y \, \varphi \)
syl l0 _