Theorem rspc3dv

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

	Ref	Expression
Hypotheses	rspc3dv.1	|- ( x = A -> ( ps <-> th ) )
	rspc3dv.2	|- ( y = B -> ( th <-> ta ) )
	rspc3dv.3	|- ( z = C -> ( ta <-> ch ) )
	rspc3dv.4	|- ( ph -> A. x e. D A. y e. E A. z e. F ps )
	rspc3dv.5	|- ( ph -> A e. D )
	rspc3dv.6	|- ( ph -> B e. E )
	rspc3dv.7	|- ( ph -> C e. F )
Assertion	rspc3dv	|- ( ph -> ch )

Proof

Step	Hyp	Ref	Expression
1		rspc3dv.1	|- ( x = A -> ( ps <-> th ) )
2		rspc3dv.2	|- ( y = B -> ( th <-> ta ) )
3		rspc3dv.3	|- ( z = C -> ( ta <-> ch ) )
4		rspc3dv.4	|- ( ph -> A. x e. D A. y e. E A. z e. F ps )
5		rspc3dv.5	|- ( ph -> A e. D )
6		rspc3dv.6	|- ( ph -> B e. E )
7		rspc3dv.7	|- ( ph -> C e. F )
8	5 6 7	3jca	|- ( ph -> ( A e. D /\ B e. E /\ C e. F ) )
9	1 2 3	rspc3v	|- ( ( A e. D /\ B e. E /\ C e. F ) -> ( A. x e. D A. y e. E A. z e. F ps -> ch ) )
10	8 4 9	sylc	|- ( ph -> ch )