Metamath Proof Explorer

Theorem rspc8v

Description: 8-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025)

Ref Expression
Hypotheses rspc8v.1 
|- ( x = A -> ( ph <-> ch ) )
rspc8v.2 
|- ( y = B -> ( ch <-> th ) )
rspc8v.3 
|- ( z = C -> ( th <-> ta ) )
rspc8v.4 
|- ( w = D -> ( ta <-> et ) )
rspc8v.5 
|- ( p = E -> ( et <-> ze ) )
rspc8v.6 
|- ( q = F -> ( ze <-> si ) )
rspc8v.7 
|- ( r = G -> ( si <-> rh ) )
rspc8v.8 
|- ( s = H -> ( rh <-> ps ) )
Assertion rspc8v 
|- ( ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) ) /\ ( ( E e. V /\ F e. W ) /\ ( G e. X /\ H e. Y ) ) ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W A. r e. X A. s e. Y ph -> ps ) )

Proof

Step Hyp Ref Expression
1 rspc8v.1 
 |-  ( x = A -> ( ph <-> ch ) )
2 rspc8v.2 
 |-  ( y = B -> ( ch <-> th ) )
3 rspc8v.3 
 |-  ( z = C -> ( th <-> ta ) )
4 rspc8v.4 
 |-  ( w = D -> ( ta <-> et ) )
5 rspc8v.5 
 |-  ( p = E -> ( et <-> ze ) )
6 rspc8v.6 
 |-  ( q = F -> ( ze <-> si ) )
7 rspc8v.7 
 |-  ( r = G -> ( si <-> rh ) )
8 rspc8v.8 
 |-  ( s = H -> ( rh <-> ps ) )
9 1 4ralbidv 
 |-  ( x = A -> ( A. p e. V A. q e. W A. r e. X A. s e. Y ph <-> A. p e. V A. q e. W A. r e. X A. s e. Y ch ) )
10 2 4ralbidv 
 |-  ( y = B -> ( A. p e. V A. q e. W A. r e. X A. s e. Y ch <-> A. p e. V A. q e. W A. r e. X A. s e. Y th ) )
11 3 4ralbidv 
 |-  ( z = C -> ( A. p e. V A. q e. W A. r e. X A. s e. Y th <-> A. p e. V A. q e. W A. r e. X A. s e. Y ta ) )
12 4 4ralbidv 
 |-  ( w = D -> ( A. p e. V A. q e. W A. r e. X A. s e. Y ta <-> A. p e. V A. q e. W A. r e. X A. s e. Y et ) )
13 9 10 11 12 rspc4v 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W A. r e. X A. s e. Y ph -> A. p e. V A. q e. W A. r e. X A. s e. Y et ) )
14 5 6 7 8 rspc4v 
 |-  ( ( ( E e. V /\ F e. W ) /\ ( G e. X /\ H e. Y ) ) -> ( A. p e. V A. q e. W A. r e. X A. s e. Y et -> ps ) )
15 13 14 sylan9 
 |-  ( ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) ) /\ ( ( E e. V /\ F e. W ) /\ ( G e. X /\ H e. Y ) ) ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W A. r e. X A. s e. Y ph -> ps ) )