Metamath Proof Explorer


Theorem spc2gv

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

Ref Expression
Hypothesis spc2egv.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
Assertion spc2gv ( ( 𝐴𝑉𝐵𝑊 ) → ( ∀ 𝑥𝑦 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 spc2egv.1 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜓 ) )
2 1 notbid ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 2 spc2egv ( ( 𝐴𝑉𝐵𝑊 ) → ( ¬ 𝜓 → ∃ 𝑥𝑦 ¬ 𝜑 ) )
4 2nalexn ( ¬ ∀ 𝑥𝑦 𝜑 ↔ ∃ 𝑥𝑦 ¬ 𝜑 )
5 3 4 syl6ibr ( ( 𝐴𝑉𝐵𝑊 ) → ( ¬ 𝜓 → ¬ ∀ 𝑥𝑦 𝜑 ) )
6 5 con4d ( ( 𝐴𝑉𝐵𝑊 ) → ( ∀ 𝑥𝑦 𝜑𝜓 ) )