Theorem rspc2dv

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

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

Proof

Step	Hyp	Ref	Expression
1		rspc2dv.1	$$⊢x=A\to \left(\psi \leftrightarrow \theta \right)$$
2		rspc2dv.2	$$⊢y=B\to \left(\theta \leftrightarrow \chi \right)$$
3		rspc2dv.3	$$⊢\phi \to \forall x\in C\forall y\in D\psi$$
4		rspc2dv.4	$$⊢\phi \to A\in C$$
5		rspc2dv.5	$$⊢\phi \to B\in D$$
6	1 2	rspc2va	$$⊢\left(\left(A\in C\wedge B\in D\right)\wedge \forall x\in C\forall y\in D\psi \right)\to \chi$$
7	4 5 3 6	syl21anc	$$⊢\phi \to \chi$$