Theorem spc2d

Description: Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017)

	Ref	Expression
Hypotheses	spc2ed.x	$$⊢Ⅎx\chi$$
	spc2ed.y	$$⊢Ⅎy\chi$$
	spc2ed.1	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	spc2d	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in W\right)\right)\to \left(\forall x\forall y\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spc2ed.x	$$⊢Ⅎx\chi$$
2		spc2ed.y	$$⊢Ⅎy\chi$$
3		spc2ed.1	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\psi \leftrightarrow \chi \right)$$
4		2nalexn	$$⊢\neg \forall x\forall y\psi \leftrightarrow \exists x\exists y\neg \psi$$
5	4	con1bii	$$⊢\neg \exists x\exists y\neg \psi \leftrightarrow \forall x\forall y\psi$$
6	1	nfn	$$⊢Ⅎx\neg \chi$$
7	2	nfn	$$⊢Ⅎy\neg \chi$$
8	3	notbid	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to \left(\neg \psi \leftrightarrow \neg \chi \right)$$
9	6 7 8	spc2ed	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in W\right)\right)\to \left(\neg \chi \to \exists x\exists y\neg \psi \right)$$
10	9	con1d	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in W\right)\right)\to \left(\neg \exists x\exists y\neg \psi \to \chi \right)$$
11	5 10	biimtrrid	$$⊢\left(\phi \wedge \left(A\in V\wedge B\in W\right)\right)\to \left(\forall x\forall y\psi \to \chi \right)$$