Metamath Proof Explorer


Theorem alexbii

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

Ref Expression
Hypothesis alexbii.1 φ ψ χ
Assertion alexbii x φ x ψ x χ

Proof

Step Hyp Ref Expression
1 alexbii.1 φ ψ χ
2 1 biimpd φ ψ χ
3 2 aleximi x φ x ψ x χ
4 1 biimprd φ χ ψ
5 4 aleximi x φ x χ x ψ
6 3 5 impbid x φ x ψ x χ