Theorem spc3gv

Description: Specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008)

	Ref	Expression
Hypothesis	spc3egv.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spc3gv	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\forall x\forall y\forall z\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		spc3egv.1	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
2	1	notbid	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
3	2	spc3egv	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\neg \psi \to \exists x\exists y\exists z\neg \phi \right)$$
4		exnal	$$⊢\exists z\neg \phi \leftrightarrow \neg \forall z\phi$$
5	4	exbii	$$⊢\exists y\exists z\neg \phi \leftrightarrow \exists y\neg \forall z\phi$$
6		exnal	$$⊢\exists y\neg \forall z\phi \leftrightarrow \neg \forall y\forall z\phi$$
7	5 6	bitri	$$⊢\exists y\exists z\neg \phi \leftrightarrow \neg \forall y\forall z\phi$$
8	7	exbii	$$⊢\exists x\exists y\exists z\neg \phi \leftrightarrow \exists x\neg \forall y\forall z\phi$$
9		exnal	$$⊢\exists x\neg \forall y\forall z\phi \leftrightarrow \neg \forall x\forall y\forall z\phi$$
10	8 9	bitr2i	$$⊢\neg \forall x\forall y\forall z\phi \leftrightarrow \exists x\exists y\exists z\neg \phi$$
11	3 10	imbitrrdi	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\neg \psi \to \neg \forall x\forall y\forall z\phi \right)$$
12	11	con4d	$$⊢\left(A\in V\wedge B\in W\wedge C\in X\right)\to \left(\forall x\forall y\forall z\phi \to \psi \right)$$