Theorem 3rspcedvd

Description: Triple application of rspcedvd . (Contributed by Steven Nguyen, 27-Feb-2023)

	Ref	Expression
Hypotheses	3rspcedvd.a	|- ( ph -> A e. D )
	3rspcedvd.b	|- ( ph -> B e. D )
	3rspcedvd.c	|- ( ph -> C e. D )
	3rspcedvd.1	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
	3rspcedvd.2	|- ( ( ph /\ y = B ) -> ( ch <-> th ) )
	3rspcedvd.3	|- ( ( ph /\ z = C ) -> ( th <-> ta ) )
	3rspcedvd.4	|- ( ph -> ta )
Assertion	3rspcedvd	|- ( ph -> E. x e. D E. y e. D E. z e. D ps )

Proof

Step	Hyp	Ref	Expression
1		3rspcedvd.a	|- ( ph -> A e. D )
2		3rspcedvd.b	|- ( ph -> B e. D )
3		3rspcedvd.c	|- ( ph -> C e. D )
4		3rspcedvd.1	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
5		3rspcedvd.2	|- ( ( ph /\ y = B ) -> ( ch <-> th ) )
6		3rspcedvd.3	|- ( ( ph /\ z = C ) -> ( th <-> ta ) )
7		3rspcedvd.4	|- ( ph -> ta )
8	4	2rexbidv	|- ( ( ph /\ x = A ) -> ( E. y e. D E. z e. D ps <-> E. y e. D E. z e. D ch ) )
9	5	rexbidv	|- ( ( ph /\ y = B ) -> ( E. z e. D ch <-> E. z e. D th ) )
10	3 6 7	rspcedvd	|- ( ph -> E. z e. D th )
11	2 9 10	rspcedvd	|- ( ph -> E. y e. D E. z e. D ch )
12	1 8 11	rspcedvd	|- ( ph -> E. x e. D E. y e. D E. z e. D ps )