# Metamath Proof Explorer

## Theorem spc2gv

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

Ref Expression
Hypothesis spc2egv.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({\phi }↔{\psi }\right)$
Assertion spc2gv ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 spc2egv.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({\phi }↔{\psi }\right)$
2 1 notbid ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left(¬{\phi }↔¬{\psi }\right)$
3 2 spc2egv ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(¬{\psi }\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)$
4 2nalexn ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
5 3 4 syl6ibr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(¬{\psi }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 5 con4d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)$