Theorem eupickbi

Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)

Conclusion
\( \vdash \exists{!} x \, \varphi \rightarrow (\exists x \, (\varphi \wedge \psi) \leftrightarrow \forall x \, (\varphi \rightarrow \psi)) \)
Proof
eupicka
l1
ex _
l2
euex
\( \vdash \exists{!} x \, \varphi \rightarrow \exists x \, \varphi \)
exintr
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \exists x \, \varphi \rightarrow \exists x \, (\varphi \wedge \psi) \)
syl5com l2 _
impbid l1 _