Frobenius rule in coherent logic
= Frobenius rule in coherent logic
{c}
{title2=$\theta\wedge\exists y\,\phi\dashv\vdash\exists y(\theta\wedge\phi)$}
When $y$ is not free in $\theta$, the coherent quantifier obeys $\theta\wedge\exists y\,\phi\dashv\vdash\exists y(\theta\wedge\phi)$. Categorically this is the interaction of existential images with pullback, ensuring stable image factorizations in a <coherent category>.