Theorem rspc3dv

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	rspc3dv.1	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
	rspc3dv.2	$$⊢y=B\to \left(\theta \leftrightarrow \tau \right)$$
	rspc3dv.3	$$⊢z=C\to \left(\tau \leftrightarrow \chi \right)$$
	rspc3dv.4	$$⊢\phi \to \forall x\in D\forall y\in E\forall z\in F\psi$$
	rspc3dv.5	$$⊢\phi \to A\in D$$
	rspc3dv.6	$$⊢\phi \to B\in E$$
	rspc3dv.7	$$⊢\phi \to C\in F$$
Assertion	rspc3dv	$$⊢\phi \to \chi$$

Proof

Step	Hyp	Ref	Expression
1		rspc3dv.1	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
2		rspc3dv.2	$$⊢y=B\to \left(\theta \leftrightarrow \tau \right)$$
3		rspc3dv.3	$$⊢z=C\to \left(\tau \leftrightarrow \chi \right)$$
4		rspc3dv.4	$$⊢\phi \to \forall x\in D\forall y\in E\forall z\in F\psi$$
5		rspc3dv.5	$$⊢\phi \to A\in D$$
6		rspc3dv.6	$$⊢\phi \to B\in E$$
7		rspc3dv.7	$$⊢\phi \to C\in F$$
8	5 6 7	3jca	$$⊢\phi \to \left(A\in D\wedge B\in E\wedge C\in F\right)$$
9	1 2 3	rspc3v	$$⊢\left(A\in D\wedge B\in E\wedge C\in F\right)\to \left(\forall x\in D\forall y\in E\forall z\in F\psi \to \chi \right)$$
10	8 4 9	sylc	$$⊢\phi \to \chi$$