Theorem 3rspcedvdw

Description: Triple application of rspcedvdw . (Contributed by SN, 20-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		3rspcedvdw.1	|- ( x = A -> ( ps <-> ch ) )
2		3rspcedvdw.2	|- ( y = B -> ( ch <-> th ) )
3		3rspcedvdw.3	|- ( z = C -> ( th <-> ta ) )
4		3rspcedvdw.a	|- ( ph -> A e. X )
5		3rspcedvdw.b	|- ( ph -> B e. Y )
6		3rspcedvdw.c	|- ( ph -> C e. Z )
7		3rspcedvdw.4	|- ( ph -> ta )
8	1 2 3	rspc3ev	|- ( ( ( A e. X /\ B e. Y /\ C e. Z ) /\ ta ) -> E. x e. X E. y e. Y E. z e. Z ps )
9	4 5 6 7 8	syl31anc	|- ( ph -> E. x e. X E. y e. Y E. z e. Z ps )