Theorem alexbii

Biconditional form of aleximi. (Contributed by BJ, 16-Nov-2020.)

Hypothesis
alexbii.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow (\exists x \, \psi \leftrightarrow \exists x \, \chi) \)
Proof
alexbii.1
biimpd _
l2
aleximi _
alexbii.1
biimprd _
aleximi _
impbid l2 _