Theorem hbe1a

Dual statement of hbe1. Modified version of axc7e with a universally quantified consequent. (Contributed by Wolf Lammen, 15-Sep-2021.)

Conclusion
\( \vdash \exists x \, \forall x \, \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
df-ex
\( \vdash \exists x \, \forall x \, \varphi \leftrightarrow \neg \forall x \, \neg \forall x \, \varphi \)
hbn1
con1i _
\( \vdash \neg \forall x \, \neg \forall x \, \varphi \rightarrow \forall x \, \varphi \)
sylbi l0 _