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