Theorem 3rspcedvdw

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

	Ref	Expression
Hypotheses	3rspcedvdw.1	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
	3rspcedvdw.2	$$⊢y=B\to \left(\chi \leftrightarrow \theta \right)$$
	3rspcedvdw.3	$$⊢z=C\to \left(\theta \leftrightarrow \tau \right)$$
	3rspcedvdw.a	$$⊢\phi \to A\in X$$
	3rspcedvdw.b	$$⊢\phi \to B\in Y$$
	3rspcedvdw.c	$$⊢\phi \to C\in Z$$
	3rspcedvdw.4	$$⊢\phi \to \tau$$
Assertion	3rspcedvdw	$$⊢\phi \to \exists x\in X\exists y\in Y\exists z\in Z\psi$$

Proof

Step	Hyp	Ref	Expression
1		3rspcedvdw.1	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
2		3rspcedvdw.2	$$⊢y=B\to \left(\chi \leftrightarrow \theta \right)$$
3		3rspcedvdw.3	$$⊢z=C\to \left(\theta \leftrightarrow \tau \right)$$
4		3rspcedvdw.a	$$⊢\phi \to A\in X$$
5		3rspcedvdw.b	$$⊢\phi \to B\in Y$$
6		3rspcedvdw.c	$$⊢\phi \to C\in Z$$
7		3rspcedvdw.4	$$⊢\phi \to \tau$$
8	1 2 3	rspc3ev	$$⊢\left(\left(A\in X\wedge B\in Y\wedge C\in Z\right)\wedge \tau \right)\to \exists x\in X\exists y\in Y\exists z\in Z\psi$$
9	4 5 6 7 8	syl31anc	$$⊢\phi \to \exists x\in X\exists y\in Y\exists z\in Z\psi$$