Theorem 3rspcedvd

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

	Ref	Expression
Hypotheses	3rspcedvd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	3rspcedvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	3rspcedvd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
	3rspcedvd.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
	3rspcedvd.2	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
	3rspcedvd.3	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐶 ) → ( 𝜃 ↔ 𝜏 ) )
	3rspcedvd.4	⊢ ( 𝜑 → 𝜏 )
Assertion	3rspcedvd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		3rspcedvd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
2		3rspcedvd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		3rspcedvd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
4		3rspcedvd.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
5		3rspcedvd.2	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( 𝜒 ↔ 𝜃 ) )
6		3rspcedvd.3	⊢ ( ( 𝜑 ∧ 𝑧 = 𝐶 ) → ( 𝜃 ↔ 𝜏 ) )
7		3rspcedvd.4	⊢ ( 𝜑 → 𝜏 )
8	4	2rexbidv	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 𝜓 ↔ ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 𝜒 ) )
9	5	rexbidv	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐵 ) → ( ∃ 𝑧 ∈ 𝐷 𝜒 ↔ ∃ 𝑧 ∈ 𝐷 𝜃 ) )
10	3 6 7	rspcedvd	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐷 𝜃 )
11	2 9 10	rspcedvd	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 𝜒 )
12	1 8 11	rspcedvd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 𝜓 )