Metamath Proof Explorer


Theorem spc2gv

Description: Specialization with two quantifiers, using implicit substitution. (Contributed by NM, 27-Apr-2004)

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

Proof

Step Hyp Ref Expression
1 spc2egv.1 x = A y = B φ ψ
2 1 notbid x = A y = B ¬ φ ¬ ψ
3 2 spc2egv A V B W ¬ ψ x y ¬ φ
4 2nalexn ¬ x y φ x y ¬ φ
5 3 4 syl6ibr A V B W ¬ ψ ¬ x y φ
6 5 con4d A V B W x y φ ψ