This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc6v

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

Ref Expression
Hypotheses rspc6v.1 
|- ( x = A -> ( ph <-> ch ) )
rspc6v.2 
|- ( y = B -> ( ch <-> th ) )
rspc6v.3 
|- ( z = C -> ( th <-> ta ) )
rspc6v.4 
|- ( w = D -> ( ta <-> et ) )
rspc6v.5 
|- ( p = E -> ( et <-> ze ) )
rspc6v.6 
|- ( q = F -> ( ze <-> ps ) )
Assertion rspc6v 
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) /\ ( E e. V /\ F e. W ) ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W ph -> ps ) )

Proof

Step Hyp Ref Expression
1 rspc6v.1 
 |-  ( x = A -> ( ph <-> ch ) )
2 rspc6v.2 
 |-  ( y = B -> ( ch <-> th ) )
3 rspc6v.3 
 |-  ( z = C -> ( th <-> ta ) )
4 rspc6v.4 
 |-  ( w = D -> ( ta <-> et ) )
5 rspc6v.5 
 |-  ( p = E -> ( et <-> ze ) )
6 rspc6v.6 
 |-  ( q = F -> ( ze <-> ps ) )
7 1 2ralbidv 
 |-  ( x = A -> ( A. p e. V A. q e. W ph <-> A. p e. V A. q e. W ch ) )
8 2 2ralbidv 
 |-  ( y = B -> ( A. p e. V A. q e. W ch <-> A. p e. V A. q e. W th ) )
9 3 2ralbidv 
 |-  ( z = C -> ( A. p e. V A. q e. W th <-> A. p e. V A. q e. W ta ) )
10 4 2ralbidv 
 |-  ( w = D -> ( A. p e. V A. q e. W ta <-> A. p e. V A. q e. W et ) )
11 7 8 9 10 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 ph -> A. p e. V A. q e. W et ) )
12 5 6 rspc2v 
 |-  ( ( E e. V /\ F e. W ) -> ( A. p e. V A. q e. W et -> ps ) )
13 11 12 syl9 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) ) -> ( ( E e. V /\ F e. W ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W ph -> ps ) ) )
14 13 3impia 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. T /\ D e. U ) /\ ( E e. V /\ F e. W ) ) -> ( A. x e. R A. y e. S A. z e. T A. w e. U A. p e. V A. q e. W ph -> ps ) )