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 ) |
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 ) |