Metamath Proof Explorer

Theorem exbii

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994)

Ref Expression
Hypothesis exbii.1 φ ψ
Assertion exbii x φ x ψ


Step Hyp Ref Expression
1 exbii.1 φ ψ
2 exbi x φ ψ x φ x ψ
3 2 1 mpg x φ x ψ