Metamath Proof Explorer

Theorem 2eximi

Description: Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005)

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


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