Metamath Proof Explorer


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 )