Metamath Proof Explorer


Theorem bj-hbyfrbi

Description: Version of bj-hbxfrbi with existential quantifiers. (Contributed by BJ, 23-Aug-2023)

Ref Expression
Assertion bj-hbyfrbi φ ψ x φ ψ x φ φ x ψ ψ

Proof

Step Hyp Ref Expression
1 exbi x φ ψ x φ x ψ
2 1 adantl φ ψ x φ ψ x φ x ψ
3 simpl φ ψ x φ ψ φ ψ
4 2 3 imbi12d φ ψ x φ ψ x φ φ x ψ ψ