Metamath Proof Explorer

Theorem eximi

Description: Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993)

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


Step Hyp Ref Expression
1 eximi.1 φ ψ
2 exim x φ ψ x φ x ψ
3 2 1 mpg x φ x ψ