# Metamath Proof Explorer

## Theorem alexbii

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

Ref Expression
Hypothesis alexbii.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
Assertion alexbii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 alexbii.1 ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
2 1 biimpd ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
3 2 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
4 1 biimprd ${⊢}{\phi }\to \left({\chi }\to {\psi }\right)$
5 4 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 3 5 impbid ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$