Metamath Proof Explorer


Theorem spc2egv

Description: Existential specialization with two quantifiers, using implicit substitution. (Contributed by NM, 3-Aug-1995)

Ref Expression
Hypothesis spc2egv.1 x = A y = B φ ψ
Assertion spc2egv A V B W ψ x y φ

Proof

Step Hyp Ref Expression
1 spc2egv.1 x = A y = B φ ψ
2 elisset A V x x = A
3 elisset B W y y = B
4 2 3 anim12i A V B W x x = A y y = B
5 exdistrv x y x = A y = B x x = A y y = B
6 4 5 sylibr A V B W x y x = A y = B
7 1 biimprcd ψ x = A y = B φ
8 7 2eximdv ψ x y x = A y = B x y φ
9 6 8 syl5com A V B W ψ x y φ