Metamath Proof Explorer


Theorem exlimddvf

Description: A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019)

Ref Expression
Hypotheses exlimddvf.1 φ x θ
exlimddvf.2 x ψ
exlimddvf.3 θ ψ χ
exlimddvf.4 x χ
Assertion exlimddvf φ ψ χ

Proof

Step Hyp Ref Expression
1 exlimddvf.1 φ x θ
2 exlimddvf.2 x ψ
3 exlimddvf.3 θ ψ χ
4 exlimddvf.4 x χ
5 3 expcom ψ θ χ
6 2 4 5 exlimd ψ x θ χ
7 1 6 mpan9 φ ψ χ