Theorem rspc2dv

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

	Ref	Expression
Hypotheses	rspc2dv.1	|- ( x = A -> ( ps <-> th ) )
	rspc2dv.2	|- ( y = B -> ( th <-> ch ) )
	rspc2dv.3	|- ( ph -> A. x e. C A. y e. D ps )
	rspc2dv.4	|- ( ph -> A e. C )
	rspc2dv.5	|- ( ph -> B e. D )
Assertion	rspc2dv	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		rspc2dv.1	|- ( x = A -> ( ps <-> th ) )
2		rspc2dv.2	|- ( y = B -> ( th <-> ch ) )
3		rspc2dv.3	|- ( ph -> A. x e. C A. y e. D ps )
4		rspc2dv.4	|- ( ph -> A e. C )
5		rspc2dv.5	|- ( ph -> B e. D )
6	1 2	rspc2va	|- ( ( ( A e. C /\ B e. D ) /\ A. x e. C A. y e. D ps ) -> ch )
7	4 5 3 6	syl21anc	|- ( ph -> ch )