Frobenius rule in coherent logic ($\theta \wedge \exists y\varphi ⊣⊢\exists y(\theta \wedge \varphi )$)

When $y$ is not free in $\theta$, the coherent quantifier obeys $\theta \wedge \exists y\varphi ⊣⊢\exists y(\theta \wedge \varphi )$. Categorically this is the interaction of existential images with pullback, ensuring stable image factorizations in a coherent category.